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

A2: now :: thesis: for i being object st i in F₁() holds
ex j being object st S₁[i,j]

let i be object ; :: thesis: ( i in F₁() implies ex j being object st S₁[j,b₂] )
assume A3: i in F₁() ; :: thesis: ex j being object st S₁[j,b₂]

per cases ( not F₃() . i is empty or F₃() . i is empty ) ;

suppose not F₃() . i is empty ; :: thesis: ex j being object st S₁[j,b₂]

then reconsider bb = F₃() . i as non empty set ;
defpred S₂[ object , object ] means P₁[$2,$1,i];
A4: for e being object st e in F₂() . i holds
ex u being object st
( u in bb & S₂[e,u] ) by A1, A3;
consider ff being Function of (F₂() . i),bb such that
A5: for e being object st e in F₂() . i holds
S₂[e,ff . e] from FUNCT_2:sch 1(A4);
reconsider fff = ff as Function of (F₂() . i),(F₃() . i) ;
reconsider j = fff as object ;
take j = j; :: thesis: S₁[i,j]
thus S₁[i,j] by A5; :: thesis: verum

end;

suppose A6: F₃() . i is empty ; :: thesis: ex j being object st S₁[j,b₂]

A7: now :: thesis: for x being object holds not x in F₂() . i

let x be object ; :: thesis: not x in F₂() . i
for y being object holds
( not y in F₃() . i or not P₁[y,x,i] ) by A6;
hence not x in F₂() . i by A1, A3; :: thesis: verum

end;

then F₂() . i = {} by XBOOLE_0:def 1;
then reconsider fff = {} as Function of (F₂() . i),(F₃() . i) by RELSET_1:12;
reconsider j = fff as object ;
take j = j; :: thesis: S₁[i,j]
thus S₁[i,j] :: thesis: verum

proof

take fff ; :: thesis: ( fff = j & ( for x being object st x in F₂() . i holds
P₁[fff . x,x,i] ) )
thus fff = j ; :: thesis: for x being object st x in F₂() . i holds
P₁[fff . x,x,i]
thus for x being object st x in F₂() . i holds
P₁[fff . x,x,i] by A7; :: thesis: verum

end;

end;

end;

end;

consider F being ManySortedSet of F₁() such that
A8: for i being object st i in F₁() holds
S₁[i,F . i] from PBOOLE:sch 3(A2);
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 f being Function of (F₂() . i),(F₃() . i) st
( f = F . i & ( for x being object st x in F₂() . i holds
P₁[f . x,x,i] ) ) by A8;
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 object st i in F₁() holds
ex f being Function of (F₂() . i),(F₃() . i) st
( f = F . i & ( for x being object st x in F₂() . i holds
P₁[f . x,x,i] ) )
thus for i being object st i in F₁() holds
ex f being Function of (F₂() . i),(F₃() . i) st
( f = F . i & ( for x being object st x in F₂() . i holds
P₁[f . x,x,i] ) ) by A8; :: thesis: verum