defpred S1[ object , object ] means ex f1 being Function of (F2() . $1),(F3() . $1) st
( f1 = $2 & ( for x being object st x in F2() . $1 holds
P1[f1 . x,x,$1] ) );
A2: now :: thesis: for i being object st i in F1() holds
ex j being object st S1[i,j]
let i be object ; :: thesis: ( i in F1() implies ex j being object st S1[j,b2] )
assume A3: i in F1() ; :: thesis: ex j being object st S1[j,b2]
per cases ( not F3() . i is empty or F3() . i is empty ) ;
suppose not F3() . i is empty ; :: thesis: ex j being object st S1[j,b2]
then reconsider bb = F3() . i as non empty set ;
defpred S2[ object , object ] means P1[$2,$1,i];
A4: for e being object st e in F2() . i holds
ex u being object st
( u in bb & S2[e,u] ) by A1, A3;
consider ff being Function of (F2() . i),bb such that
A5: for e being object st e in F2() . i holds
S2[e,ff . e] from FUNCT_2:sch 1(A4);
reconsider fff = ff as Function of (F2() . i),(F3() . i) ;
reconsider j = fff as object ;
take j = j; :: thesis: S1[i,j]
thus S1[i,j] by A5; :: thesis: verum
end;
suppose A6: F3() . i is empty ; :: thesis: ex j being object st S1[j,b2]
A7: now :: thesis: for x being object holds not x in F2() . i
let x be object ; :: thesis: not x in F2() . i
for y being object holds
( not y in F3() . i or not P1[y,x,i] ) by A6;
hence not x in F2() . i by A1, A3; :: thesis: verum
end;
then F2() . i = {} by XBOOLE_0:def 1;
then reconsider fff = {} as Function of (F2() . i),(F3() . i) by RELSET_1:12;
reconsider j = fff as object ;
take j = j; :: thesis: S1[i,j]
thus S1[i,j] :: thesis: verum
proof
take fff ; :: thesis: ( fff = j & ( for x being object st x in F2() . i holds
P1[fff . x,x,i] ) )
thus fff = j ; :: thesis: for x being object st x in F2() . i holds
P1[fff . x,x,i]
thus for x being object st x in F2() . i holds
P1[fff . x,x,i] by A7; :: thesis: verum
end;
end;
end;
end;
consider F being ManySortedSet of F1() such that
A8: for i being object st i in F1() holds
S1[i,F . i] from PBOOLE:sch 3(A2);
 F is ManySortedFunction of F2(),F3()
proof
let i be object ; :: according to PBOOLE:def 15 :: thesis: ( not i in F1() or F . i is Element of bool [:(F2() . i),(F3() . i):] )
assume i in F1() ; :: thesis: F . i is Element of bool [:(F2() . i),(F3() . i):]
then ex f being Function of (F2() . i),(F3() . i) st
( f = F . i & ( for x being object st x in F2() . i holds
P1[f . x,x,i] ) ) by A8;
hence F . i is Element of bool [:(F2() . i),(F3() . i):] ; :: thesis: verum
end;
then reconsider F = F as ManySortedFunction of F2(),F3() ;
take F ; :: thesis: for i being object st i in F1() holds
ex f being Function of (F2() . i),(F3() . i) st
( f = F . i & ( for x being object st x in F2() . i holds
P1[f . x,x,i] ) )
thus for i being object st i in F1() holds
ex f being Function of (F2() . i),(F3() . i) st
( f = F . i & ( for x being object st x in F2() . i holds
P1[f . x,x,i] ) ) by A8; :: thesis: verum