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 ex Bo1 being Subset of 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 ex Bo1 being Subset of 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 ex Bo11 being Subset of 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
for Bo1 being Subset of
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 ex Bo12 being Subset of 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 , Bo11 being Subset of , 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 , Bo12 being Subset of , 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