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
consider x1, y1 being Point of M, x2, y2 being Point of N such that
A2: ( a = [x1,x2] & b = [y1,y2] ) and
A3: 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 & 0 <= dist x2,y2 ) by METRIC_1:5;
then A4: ( the distance of M . x1,y1 = 0 & the distance of N . x2,y2 = 0 ) by A1, A3, XXREAL_0:49;
( the distance of M is discerning & the distance of N is discerning ) by METRIC_1:def 8;
then ( x1 = y1 & x2 = y2 ) by A4, METRIC_1:def 4;
hence a = b by A2; :: thesis: verum