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

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