defpred S1[ object , object ] means ( ( P1[$1] implies $2 = F3($1) ) & ( P2[$1] implies $2 = F4($1) ) & ( P3[$1] implies $2 = F5($1) ) );
defpred S2[ object ] means ( P1[$1] or P2[$1] or P3[$1] );
consider V being set such that
A2:
for x being object holds
( x in V iff ( x in F1() & S2[x] ) )
from XBOOLE_0:sch 1();
A3:
for x being object st x in V holds
ex y being object st S1[x,y]
proof
let x be
object ;
( x in V implies ex y being object st S1[x,y] )
assume A4:
x in V
;
ex y being object st S1[x,y]
then reconsider d9 =
x as
Element of
F1()
by A2;
now ex y being Element of F2() ex y being object st S1[x,y]per cases
( P1[d9] or P2[d9] or P3[d9] )
by A2, A4;
suppose A5:
P1[
d9]
;
ex y being Element of F2() ex y being object st S1[x,y]take y =
F3(
d9);
ex y being object st S1[x,y]now ex y being object st S1[x,y]per cases
( P2[d9] or not P2[d9] )
;
suppose A6:
P2[
d9]
;
ex y being object st S1[x,y]then A7:
F3(
d9)
= F4(
d9)
by A1, A5;
hence
ex
y being
object st
S1[
x,
y]
;
verum end; suppose A8:
P2[
d9]
;
ex y being object st S1[x,y]hence
ex
y being
object st
S1[
x,
y]
;
verum end; end; end; hence
ex
y being
object st
S1[
x,
y]
;
verum end; suppose A9:
P2[
d9]
;
ex y being Element of F2() ex y being object st S1[x,y]take y =
F4(
x);
ex y being object st S1[x,y]hence
ex
y being
object st
S1[
x,
y]
;
verum end; suppose A12:
P3[
d9]
;
ex y being Element of F2() ex y being object st S1[x,y]take y =
F5(
x);
ex y being object st S1[x,y]hence
ex
y being
object st
S1[
x,
y]
;
verum end; end; end;
hence
ex
y being
object st
S1[
x,
y]
;
verum
end;
consider f being Function such that
A15:
( dom f = V & ( for x being object st x in V holds
S1[x,f . x] ) )
from CLASSES1:sch 1(A3);
A16:
rng f c= F2()
V c= F1()
by A2;
then reconsider q = f as PartFunc of F1(),F2() by A15, A16, RELSET_1:4;
take
q
; ( ( for c being Element of F1() holds
( c in dom q iff ( P1[c] or P2[c] or P3[c] ) ) ) & ( for c being Element of F1() st c in dom q holds
( ( P1[c] implies q . c = F3(c) ) & ( P2[c] implies q . c = F4(c) ) & ( P3[c] implies q . c = F5(c) ) ) ) )
thus
for c being Element of F1() holds
( c in dom q iff ( P1[c] or P2[c] or P3[c] ) )
by A2, A15; for c being Element of F1() st c in dom q holds
( ( P1[c] implies q . c = F3(c) ) & ( P2[c] implies q . c = F4(c) ) & ( P3[c] implies q . c = F5(c) ) )
let i be Element of F1(); ( i in dom q implies ( ( P1[i] implies q . i = F3(i) ) & ( P2[i] implies q . i = F4(i) ) & ( P3[i] implies q . i = F5(i) ) ) )
assume
i in dom q
; ( ( P1[i] implies q . i = F3(i) ) & ( P2[i] implies q . i = F4(i) ) & ( P3[i] implies q . i = F5(i) ) )
hence
( ( P1[i] implies q . i = F3(i) ) & ( P2[i] implies q . i = F4(i) ) & ( P3[i] implies q . i = F5(i) ) )
by A15; verum