defpred S_{1}[ set , set ] means P_{1}[$1,$2];

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

for f being Element of F_{2}() st P_{1}[c,f] holds

not S_{1}[c,f]
;

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

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

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

( [c,e] in dom f iff ( P_{1}[c,e] or S_{1}[c,e] ) ) ) & ( for c being Element of F_{1}()

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

( ( P_{1}[c,g] implies f . [c,g] = F_{4}(c,g) ) & ( S_{1}[c,g] implies f . [c,g] = F_{5}(c,g) ) ) ) )
from SCHEME1:sch 15(A1);

consider g being Function such that

A3: g = f ;

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

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

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

( ( P_{1}[c,d] implies g . [c,d] = F_{4}(c,d) ) & ( P_{1}[c,d] implies g . [c,d] = F_{5}(c,d) ) )

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

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

( ( P_{1}[c,d] implies g . [c,d] = F_{4}(c,d) ) & ( P_{1}[c,d] implies g . [c,d] = F_{5}(c,d) ) )
by A2, A3; :: thesis: verum

A1: for c being Element of F

for f being Element of F

not S

consider f being PartFunc of [:F

A2: ( ( for c being Element of F

for e being Element of F

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

for g being Element of F

( ( P

consider g being Function such that

A3: g = f ;

dom f = [:F

proof

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

A4: y in F_{1}()
and

A5: z in F_{2}()
and

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

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

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

( P_{1}[y,z] or not P_{1}[y,z] )
;

hence x in dom f by A2, A6; :: 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

A4: y in F

A5: z in F

A6: 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 A2, A6; :: thesis: verum

take g ; :: thesis: for c being Element of F

for d being Element of F

( ( P

thus for c being Element of F

for d being Element of F

( ( P