let A1, A2 be non empty set ; :: thesis: for B1, B2 being set st A1 c= A2 & B1 c= B2 holds
ex F being Function of (thin_cylinders A1,B1),(thin_cylinders A2,B2) st
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 & F . x = cylinder0 A2,B2,Bo,yo2 )
let B1, B2 be set ; :: thesis: ( A1 c= A2 & B1 c= B2 implies ex F being Function of (thin_cylinders A1,B1),(thin_cylinders A2,B2) st
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 & F . x = cylinder0 A2,B2,Bo,yo2 ) )
assume AS:
( A1 c= A2 & B1 c= B2 )
; :: thesis: ex F being Function of (thin_cylinders A1,B1),(thin_cylinders A2,B2) st
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 & F . x = cylinder0 A2,B2,Bo,yo2 )
defpred S1[ set , set ] means 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 & $1 = cylinder0 A1,B1,Bo,yo1 & $2 = cylinder0 A2,B2,Bo,yo2 );
P1:
now let x be
set ;
:: thesis: ( x in thin_cylinders A1,B1 implies ex D2 being set st
( D2 in thin_cylinders A2,B2 & S1[x,D2] ) )assume
x in thin_cylinders A1,
B1
;
:: thesis: ex D2 being set st
( D2 in thin_cylinders A2,B2 & S1[x,D2] )then
ex
D being
Subset of
(Funcs B1,A1) st
(
x = D &
D is
thin_cylinder of
A1,
B1 )
;
then reconsider D1 =
x as
thin_cylinder of
A1,
B1 ;
consider Bo being
Subset of
B1,
yo1 being
Function of
Bo,
A1 such that P2:
(
Bo is
finite &
D1 = cylinder0 A1,
B1,
Bo,
yo1 )
by Def21;
D13:
Bo c= B2
by AS, XBOOLE_1:1;
reconsider yo2 =
yo1 as
Function of
Bo,
A2 by AS, FUNCT_2:9;
set D2 =
cylinder0 A2,
B2,
Bo,
yo2;
XXX:
cylinder0 A2,
B2,
Bo,
yo2 is
thin_cylinder of
A2,
B2
by P2, D13, Def21;
reconsider D2 =
cylinder0 A2,
B2,
Bo,
yo2 as
set ;
take D2 =
D2;
:: thesis: ( D2 in thin_cylinders A2,B2 & S1[x,D2] )thus
(
D2 in thin_cylinders A2,
B2 &
S1[
x,
D2] )
by P2, XXX;
:: thesis: verum end;
consider F being Function of (thin_cylinders A1,B1),(thin_cylinders A2,B2) such that
P2:
for x being set st x in thin_cylinders A1,B1 holds
S1[x,F . x]
from FUNCT_2:sch 1(P1);
take
F
; :: 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 & F . x = cylinder0 A2,B2,Bo,yo2 )
thus
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 & F . x = cylinder0 A2,B2,Bo,yo2 )
by P2; :: thesis: verum