let F1, F2 be Function of (thin_cylinders A1,B1),(thin_cylinders A2,B2); :: thesis:
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:
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:

let x be set ; :: thesis:
assume A5: x in thin_cylinders A1,B1 ; :: thesis:
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:

end;