let N be non empty ConjNormAlgStr ; :: thesis: ( N is add-associative & N is right_zeroed & N is right_complementable & N is well-conjugated & N is reflexive & N is scalar-distributive & N is scalar-unital & N is vector-distributive & N is left-distributive implies for a being Element of N holds (a *') * a = (||.a.|| ^2) * (1. N) )
assume that
A1: ( N is add-associative & N is right_zeroed & N is right_complementable ) and
A2: N is well-conjugated and
A3: N is reflexive and
A4: ( N is scalar-distributive & N is scalar-unital & N is vector-distributive & N is left-distributive ) ; :: thesis: for a being Element of N holds (a *') * a = (||.a.|| ^2) * (1. N)
let a be Element of N; :: thesis: (a *') * a = (||.a.|| ^2) * (1. N)

per cases ( not a is zero or a is zero ) ;

suppose not a is zero ; :: thesis: (a *') * a = (||.a.|| ^2) * (1. N)

hence (a *') * a = (||.a.|| ^2) * (1. N) by A2, Def3; :: thesis: verum

end;

suppose A5: a is zero ; :: thesis: (a *') * a = (||.a.|| ^2) * (1. N)

then A6: ( a = 0. N & a *' = 0. N ) by A2;
A7: ||.a.|| ^2 = 0 by A3, A5;
0 * (1. N) = 0. N by A1, A4, RLVECT_1:10;
hence (a *') * a = (||.a.|| ^2) * (1. N) by A1, A6, A4, A7; :: thesis: verum

end;

end;