let M, N be non empty Reflexive MetrStruct ; :: thesis: max-Prod2 (M,N) is Reflexive

let a be Element of (max-Prod2 (M,N)); :: according to METRIC_1:def 2,METRIC_1:def 6 :: thesis: the distance of (max-Prod2 (M,N)) . (a,a) = 0

consider x1, y1 being Point of M, x2, y2 being Point of N such that

A1: ( a = [x1,x2] & a = [y1,y2] ) and

A2: the distance of (max-Prod2 (M,N)) . (a,a) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) by Def1;

the distance of M is Reflexive by METRIC_1:def 6;

then A3: the distance of M . (x1,x1) = 0 ;

the distance of N is Reflexive by METRIC_1:def 6;

then A4: the distance of N . (x2,x2) = 0 ;

( x1 = y1 & x2 = y2 ) by A1, XTUPLE_0:1;

hence the distance of (max-Prod2 (M,N)) . (a,a) = 0 by A2, A3, A4; :: thesis: verum

let a be Element of (max-Prod2 (M,N)); :: according to METRIC_1:def 2,METRIC_1:def 6 :: thesis: the distance of (max-Prod2 (M,N)) . (a,a) = 0

consider x1, y1 being Point of M, x2, y2 being Point of N such that

A1: ( a = [x1,x2] & a = [y1,y2] ) and

A2: the distance of (max-Prod2 (M,N)) . (a,a) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) by Def1;

the distance of M is Reflexive by METRIC_1:def 6;

then A3: the distance of M . (x1,x1) = 0 ;

the distance of N is Reflexive by METRIC_1:def 6;

then A4: the distance of N . (x2,x2) = 0 ;

( x1 = y1 & x2 = y2 ) by A1, XTUPLE_0:1;

hence the distance of (max-Prod2 (M,N)) . (a,a) = 0 by A2, A3, A4; :: thesis: verum