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

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

consider B being set such that

A2: for x being object holds

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

A3: for x being object st x in B holds

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

A13: ( dom f = B & ( for y being object st y in B holds

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

A14: rng f c= F_{2}()
_{1}()
by A2;

then reconsider q = f as PartFunc of F_{1}(),F_{2}() by A13, A14, 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] or P_{3}[c] or P_{4}[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) ) & ( P_{3}[c] implies q . c = F_{5}(c) ) & ( P_{4}[c] implies q . c = F_{6}(c) ) ) ) )

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

( c in dom q iff ( P_{1}[c] or P_{2}[c] or P_{3}[c] or P_{4}[c] ) )
by A2, A13; :: 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) ) & ( P_{3}[c] implies q . c = F_{5}(c) ) & ( P_{4}[c] implies q . c = F_{6}(c) ) )

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

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

hence ( ( P_{1}[o] implies q . o = F_{3}(o) ) & ( P_{2}[o] implies q . o = F_{4}(o) ) & ( P_{3}[o] implies q . o = F_{5}(o) ) & ( P_{4}[o] implies q . o = F_{6}(o) ) )
by A13; :: thesis: verum

defpred S

consider B being set such that

A2: for x being object holds

( x in B iff ( x in F

A3: for x being object st x in B holds

ex y being object st S

proof

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

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

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

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

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

then reconsider e9 = 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] or P_{3}[x] or P_{4}[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]

A6: P_{4}[e9]
by A1, A5;

( P_{2}[e9] & P_{3}[e9] )
by A1, A5;

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

end;A6: P

( P

hence ex y being object st S

suppose A7:
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]

A8: P_{4}[e9]
by A1, A7;

( P_{1}[e9] & P_{3}[e9] )
by A1, A7;

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

end;A8: P

( P

hence ex y being object st S

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

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

A10: P_{4}[e9]
by A1, A9;

( P_{1}[e9] & P_{2}[e9] )
by A1, A9;

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

end;A10: P

( P

hence ex y being object st S

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

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

A12: P_{3}[e9]
by A1, A11;

( P_{1}[e9] & P_{2}[e9] )
by A1, A11;

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

end;A12: P

( P

hence ex y being object st S

A13: ( dom f = B & ( for y being object st y in B holds

S

A14: rng f c= F

proof

B c= 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

A15: y in dom f and

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

A15: y in dom f and

A16: 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] or P_{3}[y] or P_{4}[y] )
by A2, A13, A15;

end;

then reconsider q = f as PartFunc of F

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 o be Element of F

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

hence ( ( P