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 4,METRIC_1:def 8 :: 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 8;
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 4, METRIC_1:def 8;
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, METRIC_1:def 4; :: thesis: verum