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

defpred S_{2}[ object ] means ( P_{1}[$1] or P_{2}[$1] );

consider A being set such that

A4: for x being object holds

( x in A iff ( x in F_{1}() & S_{2}[x] ) )
from XBOOLE_0:sch 1();

A5: for x being object st x in A holds

ex y being object st S_{1}[x,y]

A10: ( dom f = A & ( for x being object st x in A holds

S_{1}[x,f . x] ) )
from CLASSES1:sch 1(A5);

A11: A c= F_{1}()
by A4;

rng f c= F_{2}()
_{1}(),F_{2}() by A11, A10, RELSET_1:4;

take f ; :: thesis: ( ( for x being object holds

( x in dom f iff ( x in F_{1}() & ( P_{1}[x] or P_{2}[x] ) ) ) ) & ( for x being object st x in dom f holds

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

thus for x being object holds

( x in dom f iff ( x in F_{1}() & ( P_{1}[x] or P_{2}[x] ) ) )
by A4, A10; :: thesis: for x being object st x in dom f holds

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

let x be object ; :: thesis: ( x in dom f implies ( ( P_{1}[x] implies f . x = F_{3}(x) ) & ( P_{2}[x] implies f . x = F_{4}(x) ) ) )

assume x in dom f ; :: thesis: ( ( P_{1}[x] implies f . x = F_{3}(x) ) & ( P_{2}[x] implies f . x = F_{4}(x) ) )

hence ( ( P_{1}[x] implies f . x = F_{3}(x) ) & ( P_{2}[x] implies f . x = F_{4}(x) ) )
by A10; :: thesis: verum

defpred S

consider A being set such that

A4: for x being object holds

( x in A iff ( x in F

A5: for x being object st x in A holds

ex y being object st S

proof

consider f being Function such that
let x be object ; :: thesis: ( x in A implies ex y being object st S_{1}[x,y] )

assume A6: x in A ; :: thesis: ex y being object st S_{1}[x,y]

then A7: x in F_{1}()
by A4;

_{1}[x,y]
; :: thesis: verum

end;assume A6: x in A ; :: thesis: ex y being object st S

then A7: x in F

now :: thesis: ex y being set ex y being object st S_{1}[x,y]end;

hence
ex y being object st Sper cases
( P_{1}[x] or P_{2}[x] )
by A4, A6;

end;

suppose A8:
P_{1}[x]
; :: thesis: ex y being set ex y being object st S_{1}[x,y]

take y = F_{3}(x); :: thesis: ex y being object st S_{1}[x,y]

P_{2}[x]
by A1, A7, A8;

hence ex y being object st S_{1}[x,y]
; :: thesis: verum

end;P

hence ex y being object st S

suppose A9:
P_{2}[x]
; :: thesis: ex y being set ex y being object st S_{1}[x,y]

take y = F_{4}(x); :: thesis: ex y being object st S_{1}[x,y]

P_{1}[x]
by A1, A7, A9;

hence ex y being object st S_{1}[x,y]
; :: thesis: verum

end;P

hence ex y being object st S

A10: ( dom f = A & ( for x being object st x in A holds

S

A11: A c= F

rng f c= F

proof

then reconsider f = f as PartFunc of F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in F_{2}() )

assume x in rng f ; :: thesis: x in F_{2}()

then consider y being object such that

A12: y in dom f and

A13: x = f . y by FUNCT_1:def 3;

_{2}()
; :: thesis: verum

end;assume x in rng f ; :: thesis: x in F

then consider y being object such that

A12: y in dom f and

A13: x = f . y by FUNCT_1:def 3;

now :: thesis: x in F_{2}()

hence
x in Fend;

take f ; :: thesis: ( ( for x being object holds

( x in dom f iff ( x in F

( ( P

thus for x being object holds

( x in dom f iff ( x in F

( ( P

let x be object ; :: thesis: ( x in dom f implies ( ( P

assume x in dom f ; :: thesis: ( ( P

hence ( ( P