let A1, A2 be non empty set ; :: thesis:
let B1, B2 be set ; :: thesis:
assume that
A1: A1 c= A2 and
A2: B1 c= B2 ; :: thesis:
defpred S₁[ 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 );

let x be set ; :: thesis:
assume x in thin_cylinders A1,B1 ; :: thesis:
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:9;
set D2 = cylinder0 A2,B2,Bo,yo2;
Bo c= B2 by A2, XBOOLE_1:1;
then A6: cylinder0 A2,B2,Bo,yo2 is thin_cylinder of A2,B2 by A4, Def2;
reconsider D2 = cylinder0 A2,B2,Bo,yo2 as set ;
take D2 = D2; :: thesis:
thus ( D2 in thin_cylinders A2,B2 & S₁[x,D2] ) by A4, A5, A6; :: thesis:

end;

consider F being Function of (thin_cylinders A1,B1),(thin_cylinders A2,B2) such that
A7: for x being set st x in thin_cylinders A1,B1 holds
S₁[x,F . x] from FUNCT_2:sch 1(A3);
take F ; :: thesis:
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; :: thesis: