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 3,METRIC_1:def 7 :: 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 7;
then A3: the distance of M . x1,x1 = 0 by METRIC_1:def 3;
the distance of N is Reflexive by METRIC_1:def 7;
then A4: the distance of N . x2,x2 = 0 by METRIC_1:def 3;
( x1 = y1 & x2 = y2 ) by A1, ZFMISC_1:33;
hence the distance of (max-Prod2 M,N) . a,a = 0 by A2, A3, A4; :: thesis: verum