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 AS1: 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 AS2: 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 AS3: x in thin_cylinders A2,B2 ; :: thesis: F1 . x = F2 . x
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
P1: ( 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 ) by AS3, AS1;
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
P2: ( 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 ) by AS3, AS2;
P3: ( Bo21 = Bo22 & yo21 = yo22 ) by LM3, P1, P2;
thus F1 . x = F2 . x by P1, P2, P3; :: thesis: verum

end;

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