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] & n = [y1,y2] ) and
A2: the distance of (max-Prod2 M,N) . m,n = max (the distance of M . x1,y1),(the distance of N . x2,y2) by Def1;
( m `1 = x1 & n `1 = y1 & m `2 = x2 & n `2 = y2 ) by A1, MCART_1:7;
hence dist m,n = max (dist (m `1 ),(n `1 )),(dist (m `2 ),(n `2 )) by A2; :: thesis: verum