let F, G be Membership_Func of C2; :: thesis: ( ( for y being Element of C2 holds F . y = min (h . [x,y]),(g . [y,z]) ) & ( for y being Element of C2 holds G . y = min (h . [x,y]),(g . [y,z]) ) implies F = G )
assume that
A12: for y being Element of C2 holds F . y = min (h . [x,y]),(g . [y,z]) and
A13: for y being Element of C2 holds G . y = min (h . [x,y]),(g . [y,z]) ; :: thesis: F = G
A14: ( dom F = C2 & dom G = C2 ) by FUNCT_2:def 1;
for y being Element of C2 st y in C2 holds
F . y = G . y

proof

let y be Element of C2; :: thesis: ( y in C2 implies F . y = G . y )
( F . y = min (h . [x,y]),(g . [y,z]) & G . y = min (h . [x,y]),(g . [y,z]) ) by A12, A13;
hence ( y in C2 implies F . y = G . y ) ; :: thesis: verum

end;

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