let F, G be Membership_Func of C; :: thesis: ( ( for c being Element of C holds F . c = (h . c) * (g . c) ) & ( for c being Element of C holds G . c = (h . c) * (g . c) ) implies F = G )

assume that

A20: for c being Element of C holds F . c = (h . c) * (g . c) and

A21: for c being Element of C holds G . c = (h . c) * (g . c) ; :: thesis: F = G

A22: for c being Element of C st c in C holds

F . c = G . c

C = dom F by FUNCT_2:def 1;

hence F = G by A23, A22, PARTFUN1:5; :: thesis: verum

assume that

A20: for c being Element of C holds F . c = (h . c) * (g . c) and

A21: for c being Element of C holds G . c = (h . c) * (g . c) ; :: thesis: F = G

A22: for c being Element of C st c in C holds

F . c = G . c

proof

A23:
C = dom G
by FUNCT_2:def 1;
let c be Element of C; :: thesis: ( c in C implies F . c = G . c )

F . c = (h . c) * (g . c) by A20;

hence ( c in C implies F . c = G . c ) by A21; :: thesis: verum

end;F . c = (h . c) * (g . c) by A20;

hence ( c in C implies F . c = G . c ) by A21; :: thesis: verum

C = dom F by FUNCT_2:def 1;

hence F = G by A23, A22, PARTFUN1:5; :: thesis: verum