let M, N be non empty MetrSpace; :: thesis: max-Prod2 (M,N) is discerning
let a, b be Element of (max-Prod2 (M,N)); :: according to METRIC_1:def 3,METRIC_1:def 7 :: thesis: ( not the distance of (max-Prod2 (M,N)) . (a,b) = 0 or a = b )
assume A1: the distance of (max-Prod2 (M,N)) . (a,b) = 0 ; :: thesis: a = b
A2: the distance of M is discerning by METRIC_1:def 7;
consider x1, y1 being Point of M, x2, y2 being Point of N such that
A3: ( a = [x1,x2] & b = [y1,y2] ) and
A4: the distance of (max-Prod2 (M,N)) . (a,b) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) by Def1;
0 <= dist (x1,y1) by METRIC_1:5;
then the distance of M . (x1,y1) = 0 by A1, A4, XXREAL_0:49;
then A5: ( the distance of N is discerning & x1 = y1 ) by A2, METRIC_1:def 7;
0 <= dist (x2,y2) by METRIC_1:5;
then the distance of N . (x2,y2) = 0 by A1, A4, XXREAL_0:49;
hence a = b by A3, A5; :: thesis: verum