defpred S_{1}[ object , object ] means ( ( P_{1}[$1] implies $2 = F_{2}($1) ) & ( P_{1}[$1] implies $2 = F_{3}($1) ) );

_{1}() such that

A4: for i being object st i in F_{1}() holds

S_{1}[i,f . i]
from PBOOLE:sch 3(A1);

take f ; :: thesis: for i being Element of F_{1}() st i in F_{1}() holds

( ( P_{1}[i] implies f . i = F_{2}(i) ) & ( P_{1}[i] implies f . i = F_{3}(i) ) )

thus for i being Element of F_{1}() st i in F_{1}() holds

( ( P_{1}[i] implies f . i = F_{2}(i) ) & ( P_{1}[i] implies f . i = F_{3}(i) ) )
by A4; :: thesis: verum

A1: now :: thesis: for i being object st i in F_{1}() holds

ex j being object st S_{1}[i,j]

consider f being ManySortedSet of Fex j being object st S

let i be object ; :: thesis: ( i in F_{1}() implies ex j being object st S_{1}[i,j] )

assume i in F_{1}()
; :: thesis: ex j being object st S_{1}[i,j]

thus ex j being object st S_{1}[i,j]
:: thesis: verum

end;assume i in F

thus ex j being object st S

proof
end;

per cases
( P_{1}[i] or not P_{1}[i] )
;

end;

A4: for i being object st i in F

S

take f ; :: thesis: for i being Element of F

( ( P

thus for i being Element of F

( ( P