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
A20: for y being Element of C2 holds F . y = min ((h . [x,y]),(g . [y,z])) and
A21: for y being Element of C2 holds G . y = min ((h . [x,y]),(g . [y,z])) ; :: thesis: F = G
A22: 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])) by A20;
hence ( y in C2 implies F . y = G . y ) by A21; :: thesis: verum

end;

A23: dom G = C2 by FUNCT_2:def 1;
dom F = C2 by FUNCT_2:def 1;
hence F = G by A23, A22, PARTFUN1:5; :: thesis: verum