defpred S₁[ object , object ] means ex f being Function of (F₂() . $1),(F₃() . $1) st
( $2 = f & ( for x being set st x in F₂() . $1 holds
( f . x in F₃() . $1 & P₁[$1,x,f . x] ) ) );
A2: for i being object st i in F₁() holds
ex y being object st S₁[i,y]

proof

let i be object ; :: thesis: ( i in F₁() implies ex y being object st S₁[i,y] )
assume A3: i in F₁() ; :: thesis: ex y being object st S₁[i,y]
defpred S₂[ object , object ] means ( $2 in F₃() . i & P₁[i,$1,$2] );

A4: now :: thesis: for x being object st x in F₂() . i holds
ex y being object st
( y in F₃() . i & S₂[x,y] )

let x be object ; :: thesis: ( x in F₂() . i implies ex y being object st
( y in F₃() . i & S₂[x,y] ) )
assume x in F₂() . i ; :: thesis: ex y being object st
( y in F₃() . i & S₂[x,y] )
then ex y being object st
( y in F₃() . i & P₁[i,x,y] ) by A1, A3;
hence ex y being object st
( y in F₃() . i & S₂[x,y] ) ; :: thesis: verum

end;

consider f being Function such that
A5: ( dom f = F₂() . i & rng f c= F₃() . i ) and
A6: for x being object st x in F₂() . i holds
S₂[x,f . x] from FUNCT_1:sch 6(A4);
reconsider f = f as Function of (F₂() . i),(F₃() . i) by A5, FUNCT_2:2;
take f ; :: thesis: S₁[i,f]
take f ; :: thesis: ( f = f & ( for x being set st x in F₂() . i holds
( f . x in F₃() . i & P₁[i,x,f . x] ) ) )
thus ( f = f & ( for x being set st x in F₂() . i holds
( f . x in F₃() . i & P₁[i,x,f . x] ) ) ) by A6; :: thesis: verum

end;

consider F being Function such that
A7: dom F = F₁() and
A8: for i being object st i in F₁() holds
S₁[i,F . i] from CLASSES1:sch 1(A2);
reconsider F = F as ManySortedSet of F₁() by A7, PARTFUN1:def 2, RELAT_1:def 18;

now :: thesis: for i being object st i in F₁() holds
F . i is Function of (F₂() . i),(F₃() . i)

let i be object ; :: thesis: ( i in F₁() implies F . i is Function of (F₂() . i),(F₃() . i) )
assume i in F₁() ; :: thesis: F . i is Function of (F₂() . i),(F₃() . i)
then ex f being Function of (F₂() . i),(F₃() . i) st
( F . i = f & ( for x being set st x in F₂() . i holds
( f . x in F₃() . i & P₁[i,x,f . x] ) ) ) by A8;
hence F . i is Function of (F₂() . i),(F₃() . i) ; :: thesis: verum

end;

then reconsider F = F as ManySortedFunction of F₂(),F₃() by PBOOLE:def 15;
take F ; :: thesis: for i, x being object st i in F₁() & x in F₂() . i holds
( (F . i) . x in F₃() . i & P₁[i,x,(F . i) . x] )
let i, x be object ; :: thesis: ( i in F₁() & x in F₂() . i implies ( (F . i) . x in F₃() . i & P₁[i,x,(F . i) . x] ) )
assume i in F₁() ; :: thesis: ( not x in F₂() . i or ( (F . i) . x in F₃() . i & P₁[i,x,(F . i) . x] ) )
then ex f being Function of (F₂() . i),(F₃() . i) st
( F . i = f & ( for x being set st x in F₂() . i holds
( f . x in F₃() . i & P₁[i,x,f . x] ) ) ) by A8;
hence ( not x in F₂() . i or ( (F . i) . x in F₃() . i & P₁[i,x,(F . i) . x] ) ) ; :: thesis: verum