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