begin
begin
theorem
canceled;
theorem
theorem Th3:
theorem
begin
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
begin
theorem
theorem
canceled;
theorem
canceled;
theorem
begin
theorem
theorem
begin
theorem
theorem
Lm1:
for I being set
for A, B being ManySortedSet of I st A is_transformable_to B holds
for H being ManySortedFunction of A,B
for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds
( H ** H1 = id B & H1 ** H = id A )
theorem
theorem
theorem