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

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

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

A1: a = [x1,x2] and

A2: 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;

consider m1, n1 being Point of M, m2, n2 being Point of N such that

A4: b = [m1,m2] and

A5: a = [n1,n2] and

A6: the distance of (max-Prod2 (M,N)) . (b,a) = max (( the distance of M . (m1,n1)),( the distance of N . (m2,n2))) by Def1;

A7: x1 = n1 by A1, A5, XTUPLE_0:1;

the distance of N is symmetric by METRIC_1:def 8;

then A8: the distance of N . (x2,y2) = the distance of N . (y2,x2) ;

the distance of M is symmetric by METRIC_1:def 8;

then A9: the distance of M . (x1,y1) = the distance of M . (y1,x1) ;

( y1 = m1 & y2 = m2 ) by A2, A4, XTUPLE_0:1;

hence the distance of (max-Prod2 (M,N)) . (a,b) = the distance of (max-Prod2 (M,N)) . (b,a) by A1, A3, A5, A6, A9, A8, A7, XTUPLE_0:1; :: thesis: verum

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

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

A1: a = [x1,x2] and

A2: 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;

consider m1, n1 being Point of M, m2, n2 being Point of N such that

A4: b = [m1,m2] and

A5: a = [n1,n2] and

A6: the distance of (max-Prod2 (M,N)) . (b,a) = max (( the distance of M . (m1,n1)),( the distance of N . (m2,n2))) by Def1;

A7: x1 = n1 by A1, A5, XTUPLE_0:1;

the distance of N is symmetric by METRIC_1:def 8;

then A8: the distance of N . (x2,y2) = the distance of N . (y2,x2) ;

the distance of M is symmetric by METRIC_1:def 8;

then A9: the distance of M . (x1,y1) = the distance of M . (y1,x1) ;

( y1 = m1 & y2 = m2 ) by A2, A4, XTUPLE_0:1;

hence the distance of (max-Prod2 (M,N)) . (a,b) = the distance of (max-Prod2 (M,N)) . (b,a) by A1, A3, A5, A6, A9, A8, A7, XTUPLE_0:1; :: thesis: verum