let F1, F2 be Function of (thin_cylinders (A2,B2)),(thin_cylinders (A1,B1)); :: thesis: ( ( for x being set st x in thin_cylinders (A2,B2) holds
ex Bo2 being Subset of B2 ex Bo1 being Subset of B1 ex yo1 being Function of Bo1,A1 ex yo2 being Function of Bo2,A2 st
( Bo1 is finite & Bo2 is finite & Bo1 = (B1 /\ Bo2) /\ (yo2 " A1) & yo1 = yo2 | Bo1 & x = cylinder0 (A2,B2,Bo2,yo2) & F1 . x = cylinder0 (A1,B1,Bo1,yo1) ) ) & ( for x being set st x in thin_cylinders (A2,B2) holds
ex Bo2 being Subset of B2 ex Bo1 being Subset of B1 ex yo1 being Function of Bo1,A1 ex yo2 being Function of Bo2,A2 st
( Bo1 is finite & Bo2 is finite & Bo1 = (B1 /\ Bo2) /\ (yo2 " A1) & yo1 = yo2 | Bo1 & x = cylinder0 (A2,B2,Bo2,yo2) & F2 . x = cylinder0 (A1,B1,Bo1,yo1) ) ) implies F1 = F2 )
assume A1: for x being set st x in thin_cylinders (A2,B2) holds
ex Bo21 being Subset of B2 ex Bo11 being Subset of B1 ex yo11 being Function of Bo11,A1 ex yo21 being Function of Bo21,A2 st
( Bo11 is finite & Bo21 is finite & Bo11 = (B1 /\ Bo21) /\ (yo21 " A1) & yo11 = yo21 | Bo11 & x = cylinder0 (A2,B2,Bo21,yo21) & F1 . x = cylinder0 (A1,B1,Bo11,yo11) ) ; :: thesis: ( ex x being set st
( x in thin_cylinders (A2,B2) & ( for Bo2 being Subset of B2
for Bo1 being Subset of B1
for yo1 being Function of Bo1,A1
for yo2 being Function of Bo2,A2 holds
( not Bo1 is finite or not Bo2 is finite or not Bo1 = (B1 /\ Bo2) /\ (yo2 " A1) or not yo1 = yo2 | Bo1 or not x = cylinder0 (A2,B2,Bo2,yo2) or not F2 . x = cylinder0 (A1,B1,Bo1,yo1) ) ) ) or F1 = F2 )
assume A2: for x being set st x in thin_cylinders (A2,B2) holds
ex Bo22 being Subset of B2 ex Bo12 being Subset of B1 ex yo12 being Function of Bo12,A1 ex yo22 being Function of Bo22,A2 st
( Bo12 is finite & Bo22 is finite & Bo12 = (B1 /\ Bo22) /\ (yo22 " A1) & yo12 = yo22 | Bo12 & x = cylinder0 (A2,B2,Bo22,yo22) & F2 . x = cylinder0 (A1,B1,Bo12,yo12) ) ; :: thesis: F1 = F2

now :: thesis: for x being object st x in thin_cylinders (A2,B2) holds
F1 . x = F2 . x

let x be object ; :: thesis: ( x in thin_cylinders (A2,B2) implies F1 . x = F2 . x )
assume A3: x in thin_cylinders (A2,B2) ; :: thesis: F1 . x = F2 . x
then consider Bo21 being Subset of B2, Bo11 being Subset of B1, yo11 being Function of Bo11,A1, yo21 being Function of Bo21,A2 such that
Bo11 is finite and
Bo21 is finite and
A4: Bo11 = (B1 /\ Bo21) /\ (yo21 " A1) and
A5: yo11 = yo21 | Bo11 and
A6: x = cylinder0 (A2,B2,Bo21,yo21) and
A7: F1 . x = cylinder0 (A1,B1,Bo11,yo11) by A1;
consider Bo22 being Subset of B2, Bo12 being Subset of B1, yo12 being Function of Bo12,A1, yo22 being Function of Bo22,A2 such that
Bo12 is finite and
Bo22 is finite and
A8: Bo12 = (B1 /\ Bo22) /\ (yo22 " A1) and
A9: yo12 = yo22 | Bo12 and
A10: x = cylinder0 (A2,B2,Bo22,yo22) and
A11: F2 . x = cylinder0 (A1,B1,Bo12,yo12) by A2, A3;
A12: yo21 = yo22 by A6, A10, Th3;
Bo21 = Bo22 by A6, A10, Th3;
hence F1 . x = F2 . x by A4, A5, A7, A8, A9, A11, A12; :: thesis: verum

end;

hence F1 = F2 by FUNCT_2:12; :: thesis: verum