let A1, A2 be non empty set ; 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 ; 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 );
A1:
now let x be
set ;
( 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
;
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 A2:
Bo2 is
finite
and A3:
D2 = cylinder0 A2,
B2,
Bo2,
yo2
by Def2;
set Bo1 =
(B1 /\ Bo2) /\ (yo2 " A1);
A4:
(B1 /\ Bo2) /\ (yo2 " A1) c= B1 /\ Bo2
by XBOOLE_1:17;
set yo1 =
yo2 | ((B1 /\ Bo2) /\ (yo2 " A1));
B1 /\ Bo2 c= Bo2
by XBOOLE_1:17;
then
(B1 /\ Bo2) /\ (yo2 " A1) c= Bo2
by A4, XBOOLE_1:1;
then A5:
yo2 | ((B1 /\ Bo2) /\ (yo2 " A1)) is
Function of
((B1 /\ Bo2) /\ (yo2 " A1)),
A2
by FUNCT_2:38;
A6:
rng (yo2 | ((B1 /\ Bo2) /\ (yo2 " A1))) = yo2 .: ((B1 /\ Bo2) /\ (yo2 " A1))
by RELAT_1:148;
A7:
yo2 .: ((B1 /\ Bo2) /\ (yo2 " A1)) c= yo2 .: (yo2 " A1)
by RELAT_1:156, XBOOLE_1:17;
yo2 .: (yo2 " A1) c= A1
by FUNCT_1:145;
then
yo2 .: ((B1 /\ Bo2) /\ (yo2 " A1)) c= A1
by A7, XBOOLE_1:1;
then reconsider yo1 =
yo2 | ((B1 /\ Bo2) /\ (yo2 " A1)) as
Function of
((B1 /\ Bo2) /\ (yo2 " A1)),
A1 by A5, A6, FUNCT_2:8;
set D1 =
cylinder0 A1,
B1,
((B1 /\ Bo2) /\ (yo2 " A1)),
yo1;
B1 /\ Bo2 c= B1
by XBOOLE_1:17;
then A8:
(B1 /\ Bo2) /\ (yo2 " A1) c= B1
by A4, XBOOLE_1:1;
then A9:
cylinder0 A1,
B1,
((B1 /\ Bo2) /\ (yo2 " A1)),
yo1 is
thin_cylinder of
A1,
B1
by A2, Def2;
reconsider D1 =
cylinder0 A1,
B1,
((B1 /\ Bo2) /\ (yo2 " A1)),
yo1 as
set ;
take D1 =
D1;
( D1 in thin_cylinders A1,B1 & S1[x,D1] )thus
(
D1 in thin_cylinders A1,
B1 &
S1[
x,
D1] )
by A2, A3, A8, A9;
verum end;
consider G being Function of (thin_cylinders A2,B2),(thin_cylinders A1,B1) such that
A10:
for x being set st x in thin_cylinders A2,B2 holds
S1[x,G . x]
from FUNCT_2:sch 1(A1);
take
G
; 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 A10; verum