let X be ComplexUnitarySpace; :: thesis: for x being Point of X holds |.(x .|. x).| = Re (x .|. x)
let x be Point of X; :: thesis: |.(x .|. x).| = Re (x .|. x)
A1: Im (x .|. x) = 0 by Def11;
Re (x .|. x) >= 0 by Def11;
then |.((Re (x .|. x)) + ((Im (x .|. x)) * <i>)).| = Re (x .|. x) by A1, ABSVALUE:def 1;
hence |.(x .|. x).| = Re (x .|. x) by COMPLEX1:13; :: thesis: verum