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;

( m `1 = x1 & n `1 = y1 ) by A1, A2;

hence dist (m,n) = max ((dist ((m `1),(n `1))),(dist ((m `2),(n `2)))) by A2, A3, A4; :: thesis: verum

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;

( m `1 = x1 & n `1 = y1 ) by A1, A2;

hence dist (m,n) = max ((dist ((m `1),(n `1))),(dist ((m `2),(n `2)))) by A2, A3, A4; :: thesis: verum