A3:
for c being Element of F_{1}()

for d being Element of F_{2}() holds

( ( P_{1}[c,d] implies not P_{2}[c,d] ) & ( P_{1}[c,d] implies not P_{3}[c,d] ) & ( P_{2}[c,d] implies not P_{3}[c,d] ) )
by A1;

consider f being PartFunc of [:F_{1}(),F_{2}():],F_{3}() such that

A4: ( ( for c being Element of F_{1}()

for b being Element of F_{2}() holds

( [c,b] in dom f iff ( P_{1}[c,b] or P_{2}[c,b] or P_{3}[c,b] ) ) ) & ( for a being Element of F_{1}()

for b being Element of F_{2}() st [a,b] in dom f holds

( ( P_{1}[a,b] implies f . [a,b] = F_{4}(a,b) ) & ( P_{2}[a,b] implies f . [a,b] = F_{5}(a,b) ) & ( P_{3}[a,b] implies f . [a,b] = F_{6}(a,b) ) ) ) )
from SCHEME1:sch 16(A3);

consider v being Function such that

A5: v = f ;

dom f = [:F_{1}(),F_{2}():]
_{1}(),F_{2}():],F_{3}() by A5, FUNCT_2:def 1;

take v ; :: thesis: ( ( for c being Element of F_{1}()

for d being Element of F_{2}() holds

( [c,d] in dom v iff ( P_{1}[c,d] or P_{2}[c,d] or P_{3}[c,d] ) ) ) & ( for c being Element of F_{1}()

for d being Element of F_{2}() st [c,d] in dom v holds

( ( P_{1}[c,d] implies v . [c,d] = F_{4}(c,d) ) & ( P_{2}[c,d] implies v . [c,d] = F_{5}(c,d) ) & ( P_{3}[c,d] implies v . [c,d] = F_{6}(c,d) ) ) ) )

thus ( ( for c being Element of F_{1}()

for d being Element of F_{2}() holds

( [c,d] in dom v iff ( P_{1}[c,d] or P_{2}[c,d] or P_{3}[c,d] ) ) ) & ( for c being Element of F_{1}()

for d being Element of F_{2}() st [c,d] in dom v holds

( ( P_{1}[c,d] implies v . [c,d] = F_{4}(c,d) ) & ( P_{2}[c,d] implies v . [c,d] = F_{5}(c,d) ) & ( P_{3}[c,d] implies v . [c,d] = F_{6}(c,d) ) ) ) )
by A4, A5; :: thesis: verum

for d being Element of F

( ( P

consider f being PartFunc of [:F

A4: ( ( for c being Element of F

for b being Element of F

( [c,b] in dom f iff ( P

for b being Element of F

( ( P

consider v being Function such that

A5: v = f ;

dom f = [:F

proof

then reconsider v = v as Function of [:F
thus
dom f c= [:F_{1}(),F_{2}():]
; :: according to XBOOLE_0:def 10 :: thesis: [:F_{1}(),F_{2}():] c= dom f

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [:F_{1}(),F_{2}():] or x in dom f )

assume x in [:F_{1}(),F_{2}():]
; :: thesis: x in dom f

then consider y, z being object such that

A6: y in F_{1}()
and

A7: z in F_{2}()
and

A8: x = [y,z] by ZFMISC_1:def 2;

reconsider z = z as Element of F_{2}() by A7;

reconsider y = y as Element of F_{1}() by A6;

( P_{1}[y,z] or P_{2}[y,z] or P_{3}[y,z] )
by A2;

hence x in dom f by A4, A8; :: thesis: verum

end;let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [:F

assume x in [:F

then consider y, z being object such that

A6: y in F

A7: z in F

A8: x = [y,z] by ZFMISC_1:def 2;

reconsider z = z as Element of F

reconsider y = y as Element of F

( P

hence x in dom f by A4, A8; :: thesis: verum

take v ; :: thesis: ( ( for c being Element of F

for d being Element of F

( [c,d] in dom v iff ( P

for d being Element of F

( ( P

thus ( ( for c being Element of F

for d being Element of F

( [c,d] in dom v iff ( P

for d being Element of F

( ( P