let F, G be Membership_Func of C; :: thesis: ( ( for c being Element of C holds F . c = abs ((h . c) - (g . c)) ) & ( for c being Element of C holds G . c = abs ((h . c) - (g . c)) ) implies F = G )
assume that
A11: for c being Element of C holds F . c = abs ((h . c) - (g . c)) and
A12: for c being Element of C holds G . c = abs ((h . c) - (g . c)) ; :: thesis: F = G
A13: ( C = dom F & C = dom G ) by FUNCT_2:def 1;
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 = abs ((h . c) - (g . c)) & G . c = abs ((h . c) - (g . c)) ) by A11, A12;
hence ( c in C implies F . c = G . c ) ; :: thesis: verum

end;

hence F = G by A13, PARTFUN1:34; :: thesis: verum