let F1, F2 be Function of (thin_cylinders (A1,B1)),(thin_cylinders (A2,B2)); :: thesis: ( ( for x being set st x in thin_cylinders (A1,B1) holds
ex Bo being Subset of B1 ex yo1 being Function of Bo,A1 ex yo2 being Function of Bo,A2 st
( Bo is finite & yo1 = yo2 & x = cylinder0 (A1,B1,Bo,yo1) & F1 . x = cylinder0 (A2,B2,Bo,yo2) ) ) & ( for x being set st x in thin_cylinders (A1,B1) holds
ex Bo being Subset of B1 ex yo1 being Function of Bo,A1 ex yo2 being Function of Bo,A2 st
( Bo is finite & yo1 = yo2 & x = cylinder0 (A1,B1,Bo,yo1) & F2 . x = cylinder0 (A2,B2,Bo,yo2) ) ) implies F1 = F2 )
assume A3: for x being set st x in thin_cylinders (A1,B1) holds
ex Bo being Subset of B1 ex yo1 being Function of Bo,A1 ex yo2 being Function of Bo,A2 st
( Bo is finite & yo1 = yo2 & x = cylinder0 (A1,B1,Bo,yo1) & F1 . x = cylinder0 (A2,B2,Bo,yo2) ) ; :: thesis: ( ex x being set st
( x in thin_cylinders (A1,B1) & ( for Bo being Subset of B1
for yo1 being Function of Bo,A1
for yo2 being Function of Bo,A2 holds
( not Bo is finite or not yo1 = yo2 or not x = cylinder0 (A1,B1,Bo,yo1) or not F2 . x = cylinder0 (A2,B2,Bo,yo2) ) ) ) or F1 = F2 )
assume A4: for x being set st x in thin_cylinders (A1,B1) holds
ex Bo being Subset of B1 ex yo1 being Function of Bo,A1 ex yo2 being Function of Bo,A2 st
( Bo is finite & yo1 = yo2 & x = cylinder0 (A1,B1,Bo,yo1) & F2 . x = cylinder0 (A2,B2,Bo,yo2) ) ; :: thesis: F1 = F2

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

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

end;

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