let M, N be non empty MetrStruct ; :: thesis: for m, n being Point of (max-Prod2 M,N) holds dist m,n = max (dist (m `1 ),(n `1 )),(dist (m `2 ),(n `2 ))
let m, n be Point of (max-Prod2 M,N); :: thesis: dist m,n = max (dist (m `1 ),(n `1 )),(dist (m `2 ),(n `2 ))
consider x1, y1 being Point of M, x2, y2 being Point of N such that
A1: m = [x1,x2] and
A2: n = [y1,y2] and
A3: the distance of (max-Prod2 M,N) . m,n = max (the distance of M . x1,y1),(the distance of N . x2,y2) by Def1;
A4: m `2 = x2 by A1, MCART_1:7;
( m `1 = x1 & n `1 = y1 ) by A1, A2, MCART_1:7;
hence dist m,n = max (dist (m `1 ),(n `1 )),(dist (m `2 ),(n `2 )) by A2, A3, A4, MCART_1:7; :: thesis: verum