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

A2: for x being object holds

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

A3: for x being object st x in V holds

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

A15: ( dom f = V & ( for x being object st x in V holds

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

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

then reconsider q = f as PartFunc of F_{1}(),F_{2}() by A15, A16, 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, A15; :: 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 i be Element of F_{1}(); :: thesis: ( i in dom q implies ( ( P_{1}[i] implies q . i = F_{3}(i) ) & ( P_{2}[i] implies q . i = F_{4}(i) ) & ( P_{3}[i] implies q . i = F_{5}(i) ) ) )

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

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

defpred S

consider V being set such that

A2: for x being object holds

( x in V iff ( x in F

A3: for x being object st x in V holds

ex y being object st S

proof

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

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

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

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

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

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

end;

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

take y = F_{3}(d9); :: 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}[d9] or not P_{2}[d9] )
;

end;

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

then A7:
F_{3}(d9) = F_{4}(d9)
by A1, A5;

_{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_{3}[d9] or not P_{3}[d9] )
;

end;

suppose A8:
P_{2}[d9]
; :: 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_{3}[d9] or not P_{3}[d9] )
;

end;

suppose A9:
P_{2}[d9]
; :: 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]

_{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}[d9] or not P_{1}[d9] )
;

end;

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

then A10:
F_{3}(d9) = F_{4}(d9)
by A1, A9;

_{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_{3}[d9] or not P_{3}[d9] )
;

end;

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

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

end;

per cases
( P_{3}[d9] or not P_{3}[d9] )
;

end;

suppose A12:
P_{3}[d9]
; :: 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]

_{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}[d9] or not P_{1}[d9] )
;

end;

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

then A13:
F_{3}(d9) = F_{5}(d9)
by A1, A12;

_{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}[d9] or not P_{2}[d9] )
;

end;

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

then
F_{4}(d9) = F_{5}(d9)
by A1, A12;

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

end;hence ex y being object st S

suppose A14:
P_{1}[d9]
; :: 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}[d9] or not P_{2}[d9] )
;

end;

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

then
F_{4}(d9) = F_{5}(d9)
by A1, A12;

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

end;hence ex y being object st S

A15: ( dom f = V & ( for x being object st x in V holds

S

A16: rng f c= F

proof

V 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

A17: y in dom f and

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

A17: y in dom f and

A18: 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, A15, A17;

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

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

hence ( ( P