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

let x be set ; :: 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:18; :: thesis: verum