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 X being set such that

A2: for x being object holds

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

A3: for x being object st x in X holds

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

A7: ( dom f = X & ( for x being object st x in X holds

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

A8: X c= F_{1}()
by A2;

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

take q ; :: thesis: ( ( for c being Element of F_{1}() holds

( c in dom q iff ( P_{1}[c] or P_{2}[c] ) ) ) & ( for c being Element of F_{1}() st c in dom q holds

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

thus for c being Element of F_{1}() holds

( c in dom q iff ( P_{1}[c] or P_{2}[c] ) )
by A2, A7; :: thesis: for c being Element of F_{1}() st c in dom q holds

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

let b be Element of F_{1}(); :: thesis: ( b in dom q implies ( ( P_{1}[b] implies q . b = F_{3}(b) ) & ( P_{2}[b] implies q . b = F_{4}(b) ) ) )

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

hence ( ( P_{1}[b] implies q . b = F_{3}(b) ) & ( P_{2}[b] implies q . b = F_{4}(b) ) )
by A7; :: thesis: verum

defpred S

consider X being set such that

A2: for x being object holds

( x in X iff ( x in F

A3: for x being object st x in X holds

ex y being object st S

proof

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

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

then reconsider x9 = x as Element of F_{1}() by A2;

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

end;assume A4: x in X ; :: thesis: ex y being object st S

then reconsider x9 = x as Element of F

now :: thesis: ex y being Element of F_{2}() 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 A2, A4;

end;

suppose A5:
P_{1}[x]
; :: thesis: ex y being Element of F_{2}() 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}[x9]
by A1, A5;

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

end;P

hence ex y being object st S

suppose A6:
P_{2}[x]
; :: thesis: ex y being Element of F_{2}() 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}[x9]
by A1, A6;

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

end;P

hence ex y being object st S

A7: ( dom f = X & ( for x being object st x in X holds

S

A8: X c= F

rng f c= F

proof

then reconsider q = 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

A9: y in dom f and

A10: 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

A9: y in dom f and

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

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

hence
x in Fper cases
( P_{1}[y] or P_{2}[y] )
by A2, A7, A9;

end;

take q ; :: thesis: ( ( for c being Element of F

( c in dom q iff ( P

( ( P

thus for c being Element of F

( c in dom q iff ( P

( ( P

let b be Element of F

assume b in dom q ; :: thesis: ( ( P

hence ( ( P