let p1, p2 be Point of (TOP-REAL 2); :: thesis: |(p1,p2)| = Re ((euc2cpx p1) .|. (euc2cpx p2))
A1: ( p1 `1 = Re (euc2cpx p1) & p1 `2 = Im (euc2cpx p1) ) by COMPLEX1:28;
A2: ( p2 `1 = Re (euc2cpx p2) & p2 `2 = Im (euc2cpx p2) ) by COMPLEX1:28;
thus |(p1,p2)| = ((p1 `1 ) * (p2 `1 )) + ((p1 `2 ) * (p2 `2 )) by Th50
.= Re ((euc2cpx p1) .|. (euc2cpx p2)) by A1, A2, Th48 ; :: thesis: verum