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 Z being set such that
A2:
for x being object holds
( x in Z iff ( x in F1() & S2[x] ) )
from XBOOLE_0:sch 1();
A3:
for x being object st x in Z holds
ex y being object st S1[x,y]
proof
let x be
object ;
( x in Z implies ex y being object st S1[x,y] )
assume A4:
x in Z
;
ex y being object st S1[x,y]
then reconsider c9 =
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[x] or P2[x] or P3[x] )
by A2, A4;
suppose A5:
P1[
x]
;
ex y being Element of F2() ex y being object st S1[x,y]take y =
F3(
x);
ex y being object st S1[x,y]
(
P2[
c9] &
P3[
c9] )
by A1, A5;
hence
ex
y being
object st
S1[
x,
y]
;
verum end; suppose A6:
P2[
x]
;
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]
(
P1[
c9] &
P3[
c9] )
by A1, A6;
hence
ex
y being
object st
S1[
x,
y]
;
verum end; suppose A7:
P3[
x]
;
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]
(
P1[
c9] &
P2[
c9] )
by A1, A7;
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
A8:
( dom f = Z & ( for x being object st x in Z holds
S1[x,f . x] ) )
from CLASSES1:sch 1(A3);
A9:
rng f c= F2()
Z c= F1()
by A2;
then reconsider q = f as PartFunc of F1(),F2() by A8, A9, 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, A8; 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 g be Element of F1(); ( g in dom q implies ( ( P1[g] implies q . g = F3(g) ) & ( P2[g] implies q . g = F4(g) ) & ( P3[g] implies q . g = F5(g) ) ) )
assume
g in dom q
; ( ( P1[g] implies q . g = F3(g) ) & ( P2[g] implies q . g = F4(g) ) & ( P3[g] implies q . g = F5(g) ) )
hence
( ( P1[g] implies q . g = F3(g) ) & ( P2[g] implies q . g = F4(g) ) & ( P3[g] implies q . g = F5(g) ) )
by A8; verum