let F, G be Membership_Func of C; :: thesis: ( ( for c being Element of C holds F . c = ((h . c) + (g . c)) - ((h . c) * (g . c)) ) & ( for c being Element of C holds G . c = ((h . c) + (g . c)) - ((h . c) * (g . c)) ) implies F = G )
assume that
A15: for c being Element of C holds F . c = ((h . c) + (g . c)) - ((h . c) * (g . c)) and
A16: for c being Element of C holds G . c = ((h . c) + (g . c)) - ((h . c) * (g . c)) ; :: thesis: F = G
A17: for c being Element of C st c in C holds
F . c = G . c

proof

let c be Element of C; :: thesis: ( c in C implies F . c = G . c )
F . c = ((h . c) + (g . c)) - ((h . c) * (g . c)) by A15;
hence ( c in C implies F . c = G . c ) by A16; :: thesis: verum

end;

A18: C = dom G by FUNCT_2:def 1;
C = dom F by FUNCT_2:def 1;
hence F = G by A18, A17, PARTFUN1:5; :: thesis: verum