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

A6: for x being object holds

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

A7: for x being object st x in D holds

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

A18: ( dom f = D & ( for x being object st x in D holds

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

A19: D c= F_{1}()
by A6;

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

take f ; :: thesis: ( ( for x being object holds

( x in dom f iff ( x in F_{1}() & ( P_{1}[x] or P_{2}[x] or P_{3}[x] or P_{4}[x] ) ) ) ) & ( for x being object st x in dom f holds

( ( P_{1}[x] implies f . x = F_{3}(x) ) & ( P_{2}[x] implies f . x = F_{4}(x) ) & ( P_{3}[x] implies f . x = F_{5}(x) ) & ( P_{4}[x] implies f . x = F_{6}(x) ) ) ) )

thus for x being object holds

( x in dom f iff ( x in F_{1}() & ( P_{1}[x] or P_{2}[x] or P_{3}[x] or P_{4}[x] ) ) )
by A6, A18; :: thesis: for x being object st x in dom f holds

( ( P_{1}[x] implies f . x = F_{3}(x) ) & ( P_{2}[x] implies f . x = F_{4}(x) ) & ( P_{3}[x] implies f . x = F_{5}(x) ) & ( P_{4}[x] implies f . x = F_{6}(x) ) )

let x be object ; :: thesis: ( x in dom f implies ( ( P_{1}[x] implies f . x = F_{3}(x) ) & ( P_{2}[x] implies f . x = F_{4}(x) ) & ( P_{3}[x] implies f . x = F_{5}(x) ) & ( P_{4}[x] implies f . x = F_{6}(x) ) ) )

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

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

defpred S

consider D being set such that

A6: for x being object holds

( x in D iff ( x in F

A7: for x being object st x in D holds

ex y being object st S

proof

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

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

then A9: x in F_{1}()
by A6;

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

end;assume A8: x in D ; :: thesis: ex y being object st S

then A9: x in F

now :: thesis: ex y being set 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 A6, A8;

end;

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

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

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

( P_{2}[x] & P_{3}[x] )
by A1, A9, A10;

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

end;A11: P

( P

hence ex y being object st S

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

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

A13: P_{4}[x]
by A1, A9, A12;

( P_{1}[x] & P_{3}[x] )
by A1, A9, A12;

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

end;A13: P

( P

hence ex y being object st S

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

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

A15: P_{4}[x]
by A1, A9, A14;

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

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

end;A15: P

( P

hence ex y being object st S

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

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

A17: P_{3}[x]
by A1, A9, A16;

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

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

end;A17: P

( P

hence ex y being object st S

A18: ( dom f = D & ( for x being object st x in D holds

S

A19: D c= F

rng f c= F

proof

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

A20: y in dom f and

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

A20: y in dom f and

A21: 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 A6, A18, A20;

end;

suppose A22:
P_{1}[y]
; :: thesis: x in F_{2}()

then
f . y = F_{3}(y)
by A18, A20;

hence x in F_{2}()
by A2, A19, A18, A20, A21, A22; :: thesis: verum

end;hence x in F

suppose A23:
P_{2}[y]
; :: thesis: x in F_{2}()

then
f . y = F_{4}(y)
by A18, A20;

hence x in F_{2}()
by A3, A19, A18, A20, A21, A23; :: thesis: verum

end;hence x in F

take f ; :: thesis: ( ( for x being object holds

( x in dom f iff ( x in F

( ( P

thus for x being object holds

( x in dom f iff ( x in F

( ( P

let x be object ; :: thesis: ( x in dom f implies ( ( P

assume x in dom f ; :: thesis: ( ( P

hence ( ( P