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) ) );

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

consider Z being set such that

A2: for x being object holds

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

A3: for x being object st x in Z holds

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

A8: ( dom f = Z & ( for x being object st x in Z holds

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

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

then reconsider q = f as PartFunc of F_{1}(),F_{2}() by A8, A9, 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] ) ) ) & ( 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) ) ) ) )

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] ) )
by A2, A8; :: 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) ) )

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

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

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

defpred S

consider Z being set such that

A2: for x being object holds

( x in Z iff ( x in F

A3: for x being object st x in Z holds

ex y being object st S

proof

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

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

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

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

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

then reconsider c9 = 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] )
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}[c9] & P_{3}[c9] )
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}[c9] & P_{3}[c9] )
by A1, A6;

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

end;( P

hence ex y being object st S

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

( P_{1}[c9] & P_{2}[c9] )
by A1, A7;

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

end;( P

hence ex y being object st S

A8: ( dom f = Z & ( for x being object st x in Z holds

S

A9: rng f c= F

proof

Z 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

A10: y in dom f and

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

A10: y in dom f and

A11: 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] )
by A2, A8, A10;

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

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

hence ( ( P