defpred S₁[ object , object ] means ex g being Function of (F₂() . $1),(F₃() . $1) st
( $2 = g & ( for a being set st a in F₂() . $1 holds
P₁[$1,a,g . a] ) );
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 i in F₁() ; :: thesis: ex y being object st S₁[i,y]
then reconsider ii = i as Element of F₁() ;
defpred S₂[ object , object ] means P₁[i,$1,$2];
A3: for a being object st a in F₂() . i holds
ex b being object st
( b in F₃() . i & S₂[a,b] )

proof

let a be object ; :: thesis: ( a in F₂() . i implies ex b being object st
( b in F₃() . i & S₂[a,b] ) )
assume a in F₂() . i ; :: thesis: ex b being object st
( b in F₃() . i & S₂[a,b] )
then ex b being Element of F₃() . ii st P₁[i,a,b] by A1;
hence ex b being object st
( b in F₃() . i & S₂[a,b] ) ; :: thesis: verum

end;

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

end;

consider f being Function such that
A6: dom f = F₁() and
A7: 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 A6, PARTFUN1:def 2, RELAT_1:def 18;
f is ManySortedFunction of F₂(),F₃()

proof

let i be object ; :: according to PBOOLE:def 15 :: thesis: ( not i in F₁() or f . i is Element of bool [:(F₂() . i),(F₃() . i):] )
assume i in F₁() ; :: thesis: f . i is Element of bool [:(F₂() . i),(F₃() . i):]
then ex g being Function of (F₂() . i),(F₃() . i) st
( f . i = g & ( for a being set st a in F₂() . i holds
P₁[i,a,g . a] ) ) by A7;
hence f . i is Element of bool [:(F₂() . i),(F₃() . i):] ; :: thesis: verum

end;

then reconsider f = f as ManySortedFunction of F₂(),F₃() ;
take f ; :: thesis: for i being Element of F₁()
for a being Element of F₂() . i holds P₁[i,a,(f . i) . a]
let i be Element of F₁(); :: thesis: for a being Element of F₂() . i holds P₁[i,a,(f . i) . a]
let a be Element of F₂() . i; :: thesis: P₁[i,a,(f . i) . a]
ex g being Function of (F₂() . i),(F₃() . i) st
( f . i = g & ( for a being set st a in F₂() . i holds
P₁[i,a,g . a] ) ) by A7;
hence P₁[i,a,(f . i) . a] ; :: thesis: verum