Next: QUOTIENT Up: The Rules Previous: FUNCTION

# PRODUCT

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

* formation . H >> ext x:A#B by intro product A new x
* >> A in
* x:A >> ext B

. 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

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

. 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

* noncanonical . H,z:(x:A#B), >> T ext spread(z;u,v.t) by elim z new u,v
* u:A,v:B[u/x] ,z=<u,v> in x:A#B >> T[<u,v>/z] ext t

. 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

* computation . H >> spread(<a,b>;) = s in T by reduce 1
* >> t[a,b/x,y] = s in T

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995