let A1, A2 be non empty set ; 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 ; ( 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 that
A1:
A1 c= A2
and
A2:
B1 c= B2
; 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[ object , object ] 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) );
A3:
now for x being object st x in thin_cylinders (A1,B1) holds
ex D2 being object st
( D2 in thin_cylinders (A2,B2) & S1[x,D2] )let x be
object ;
( x in thin_cylinders (A1,B1) implies ex D2 being object st
( D2 in thin_cylinders (A2,B2) & S1[x,D2] ) )assume
x in thin_cylinders (
A1,
B1)
;
ex D2 being object 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 A4:
Bo is
finite
and A5:
D1 = cylinder0 (
A1,
B1,
Bo,
yo1)
by Def2;
reconsider yo2 =
yo1 as
Function of
Bo,
A2 by A1, FUNCT_2:7;
set D2 =
cylinder0 (
A2,
B2,
Bo,
yo2);
Bo c= B2
by A2;
then A6:
cylinder0 (
A2,
B2,
Bo,
yo2) is
thin_cylinder of
A2,
B2
by A4, Def2;
reconsider D2 =
cylinder0 (
A2,
B2,
Bo,
yo2) as
object ;
take D2 =
D2;
( D2 in thin_cylinders (A2,B2) & S1[x,D2] )thus
(
D2 in thin_cylinders (
A2,
B2) &
S1[
x,
D2] )
by A4, A5, A6;
verum end;
consider F being Function of (thin_cylinders (A1,B1)),(thin_cylinders (A2,B2)) such that
A7:
for x being object st x in thin_cylinders (A1,B1) holds
S1[x,F . x]
from FUNCT_2:sch 1(A3);
take
F
; 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 A7; verum