let A1, A2 be non empty set ; :: thesis: for B1, B2 being set ex G being Function of (thin_cylinders A2,B2),(thin_cylinders A1,B1) st
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 & G . x = cylinder0 A1,B1,Bo1,yo1 )
let B1, B2 be set ; :: thesis: ex G being Function of (thin_cylinders A2,B2),(thin_cylinders A1,B1) st
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 & G . x = cylinder0 A1,B1,Bo1,yo1 )
defpred S1[ set , set ] means 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 & $1 = cylinder0 A2,B2,Bo2,yo2 & $2 = cylinder0 A1,B1,Bo1,yo1 );
P1:
now let x be
set ;
:: thesis: ( x in thin_cylinders A2,B2 implies ex D1 being set st
( D1 in thin_cylinders A1,B1 & S1[x,D1] ) )assume
x in thin_cylinders A2,
B2
;
:: thesis: ex D1 being set st
( D1 in thin_cylinders A1,B1 & S1[x,D1] )then
ex
D being
Subset of
(Funcs B2,A2) st
(
x = D &
D is
thin_cylinder of
A2,
B2 )
;
then reconsider D2 =
x as
thin_cylinder of
A2,
B2 ;
consider Bo2 being
Subset of
B2,
yo2 being
Function of
Bo2,
A2 such that P2:
(
Bo2 is
finite &
D2 = cylinder0 A2,
B2,
Bo2,
yo2 )
by Def21;
set Bo1 =
(B1 /\ Bo2) /\ (yo2 " A1);
XXX:
(B1 /\ Bo2) /\ (yo2 " A1) c= B1 /\ Bo2
by XBOOLE_1:17;
B1 /\ Bo2 c= B1
by XBOOLE_1:17;
then D13:
(B1 /\ Bo2) /\ (yo2 " A1) c= B1
by XXX, XBOOLE_1:1;
B1 /\ Bo2 c= Bo2
by XBOOLE_1:17;
then YYY:
(B1 /\ Bo2) /\ (yo2 " A1) c= Bo2
by XXX, XBOOLE_1:1;
set yo1 =
yo2 | ((B1 /\ Bo2) /\ (yo2 " A1));
ZZZ:
yo2 | ((B1 /\ Bo2) /\ (yo2 " A1)) is
Function of
((B1 /\ Bo2) /\ (yo2 " A1)),
A2
by YYY, FUNCT_2:38;
W1:
yo2 .: (yo2 " A1) c= A1
by FUNCT_1:145;
W2:
rng (yo2 | ((B1 /\ Bo2) /\ (yo2 " A1))) = yo2 .: ((B1 /\ Bo2) /\ (yo2 " A1))
by RELAT_1:148;
yo2 .: ((B1 /\ Bo2) /\ (yo2 " A1)) c= yo2 .: (yo2 " A1)
by RELAT_1:156, XBOOLE_1:17;
then
yo2 .: ((B1 /\ Bo2) /\ (yo2 " A1)) c= A1
by W1, XBOOLE_1:1;
then reconsider yo1 =
yo2 | ((B1 /\ Bo2) /\ (yo2 " A1)) as
Function of
((B1 /\ Bo2) /\ (yo2 " A1)),
A1 by ZZZ, W2, FUNCT_2:8;
set D1 =
cylinder0 A1,
B1,
((B1 /\ Bo2) /\ (yo2 " A1)),
yo1;
XXX:
cylinder0 A1,
B1,
((B1 /\ Bo2) /\ (yo2 " A1)),
yo1 is
thin_cylinder of
A1,
B1
by D13, P2, Def21;
reconsider D1 =
cylinder0 A1,
B1,
((B1 /\ Bo2) /\ (yo2 " A1)),
yo1 as
set ;
take D1 =
D1;
:: thesis: ( D1 in thin_cylinders A1,B1 & S1[x,D1] )thus
(
D1 in thin_cylinders A1,
B1 &
S1[
x,
D1] )
by P2, XXX, D13;
:: thesis: verum end;
consider G being Function of (thin_cylinders A2,B2),(thin_cylinders A1,B1) such that
P2:
for x being set st x in thin_cylinders A2,B2 holds
S1[x,G . x]
from FUNCT_2:sch 1(P1);
take
G
; :: 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 & G . x = cylinder0 A1,B1,Bo1,yo1 )
thus
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 & G . x = cylinder0 A1,B1,Bo1,yo1 )
by P2; :: thesis: verum