Nuprl - DiscreteMath LEMMAs for function_functionality_wrt_one_one

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Theorem	Name
Thm* (A ~ A') (B ~ B') ((AB) ~ (A'B'))	[function_functionality_wrt_one_one_corr]
cites the following:
Thm* (A ~ A') (B ~ B') (:A. B) ~ (:A'. B')	[one_one_corr_fams_indep_if_one_one_corr]
Thm* (x:A. B(x)) ~ (x:A'. B'(x)) ((x:AB(x)) ~ (x:A'B'(x)))	[card_pi]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html