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[ object , object ] 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 for x being object st x in thin_cylinders (A2,B2) holds
ex D1 being object st
( D1 in thin_cylinders (A1,B1) & S1[x,D1] )let x be
object ;
( x in thin_cylinders (A2,B2) implies ex D1 being object st
( D1 in thin_cylinders (A1,B1) & S1[x,D1] ) )assume
x in thin_cylinders (
A2,
B2)
;
ex D1 being object 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;
then A5:
yo2 | ((B1 /\ Bo2) /\ (yo2 " A1)) is
Function of
((B1 /\ Bo2) /\ (yo2 " A1)),
A2
by FUNCT_2:32;
A6:
rng (yo2 | ((B1 /\ Bo2) /\ (yo2 " A1))) = yo2 .: ((B1 /\ Bo2) /\ (yo2 " A1))
by RELAT_1:115;
A7:
yo2 .: ((B1 /\ Bo2) /\ (yo2 " A1)) c= yo2 .: (yo2 " A1)
by RELAT_1:123, XBOOLE_1:17;
yo2 .: (yo2 " A1) c= A1
by FUNCT_1:75;
then
yo2 .: ((B1 /\ Bo2) /\ (yo2 " A1)) c= A1
by A7;
then reconsider yo1 =
yo2 | ((B1 /\ Bo2) /\ (yo2 " A1)) as
Function of
((B1 /\ Bo2) /\ (yo2 " A1)),
A1 by A5, A6, FUNCT_2:6;
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;
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
object ;
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 object 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