let F1, F2 be Function of (thin_cylinders (A2,B2)),(thin_cylinders (A1,B1)); ( ( 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) )
; ( 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) )
; F1 = F2
now for x being object st x in thin_cylinders (A2,B2) holds
F1 . x = F2 . xlet x be
object ;
( x in thin_cylinders (A2,B2) implies F1 . x = F2 . x )assume A3:
x in thin_cylinders (
A2,
B2)
;
F1 . x = F2 . xthen 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;
verum end;
hence
F1 = F2
by FUNCT_2:12; verum