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 AS1:
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 AS2:
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 let x be
set ;
:: thesis: ( x in thin_cylinders A1,B1 implies F1 . x = F2 . x )assume AS3:
x in thin_cylinders A1,
B1
;
:: thesis: F1 . x = F2 . xconsider Bo1 being
Subset of
B1,
yo11 being
Function of
Bo1,
A1,
yo21 being
Function of
Bo1,
A2 such that P1:
(
Bo1 is
finite &
yo11 = yo21 &
x = cylinder0 A1,
B1,
Bo1,
yo11 &
F1 . x = cylinder0 A2,
B2,
Bo1,
yo21 )
by AS3, AS1;
consider Bo2 being
Subset of
B1,
yo12 being
Function of
Bo2,
A1,
yo22 being
Function of
Bo2,
A2 such that P2:
(
Bo2 is
finite &
yo12 = yo22 &
x = cylinder0 A1,
B1,
Bo2,
yo12 &
F2 . x = cylinder0 A2,
B2,
Bo2,
yo22 )
by AS3, AS2;
P3:
(
Bo1 = Bo2 &
yo11 = yo12 )
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