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

A2: for x being object holds

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

A3: for x being object st x in Y holds

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

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

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

A8: Y 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 e be Element of F_{1}(); :: thesis: ( e in dom q implies ( ( P_{1}[e] implies q . e = F_{3}(e) ) & ( P_{2}[e] implies q . e = F_{4}(e) ) ) )

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

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

defpred S

consider Y being set such that

A2: for x being object holds

( x in Y iff ( x in F

A3: for x being object st x in Y holds

ex y being object st S

proof

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

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

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

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

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

then reconsider a9 = 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}[a9] or P_{2}[a9] )
by A2, A4;

end;

suppose A5:
P_{1}[a9]
; :: thesis: ex y being Element of F_{2}() ex y being object st S_{1}[x,y]

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

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

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

hence
ex y being object st Sper cases
( P_{2}[a9] or not P_{2}[a9] )
;

end;

suppose A6:
P_{2}[a9]
; :: thesis: ex y being Element of F_{2}() ex y being object st S_{1}[x,y]

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

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

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

hence
ex y being object st Sper cases
( P_{1}[a9] or not P_{1}[a9] )
;

end;

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

S

A8: Y 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 e be Element of F

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

hence ( ( P