rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* >>

*

.`
H >> x:A#B in
by intro [new y] `

* >> A in

* y:A >> B[y/x] in

`
.
H >>
ext A#B by intro product `

* >> ext A

* >> ext B

`
.
H >> A#B in
by intro `

* >> A in

* >> B in

`
rulesubsection23.25ex plus
1ex minus .2ex1.5ex plus .2ex`

* >>

* >>

*

.`
H >> <a,b> in x:A#B by intro at
[new y] `

* >> a in A

* >> b in B[a/x]

* y:A >> B[y/x] in

`
.
H >> A#B ext <a,b> by intro `

* >> A ext a

* >> B ext b

`
.
H >> <a,b> in A#B by intro `

* >> a in A

* >> b in B

`
rulesubsection23.25ex plus
1ex minus .2ex1.5ex plus .2ex`

*

.`
H >> spread(e;) in T[e/z]
`

* by intro [over ] using w:A#B [new u,v]

* >> e in w:A#B

* u:A,v:B[u/w] ,e=<u,v> in w:A#B >> t[u,v/x,y] in T[<u,v>/z]

`
rulesubsection23.25ex plus
1ex minus .2ex1.5ex plus .2ex`

* >>

`
`

Thu Sep 14 08:45:18 EDT 1995