begin
Lm1:
for I being set
for A, B, C being ManySortedSet of I
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C holds G ** F is ManySortedSet of I
begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem Th8:
theorem
theorem
begin
theorem
theorem
theorem
theorem
theorem
begin
theorem Th16:
theorem Th17:
begin
theorem Th18:
theorem
theorem
theorem
theorem
theorem