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

suppose A1: not a is zero ; :: thesis: (a *') *' = a

then A2: (a *') * a = (||.a.|| ^2) * (1. N) by Def3;
A3: ((a *') *') * (a *') = (||.(a *').|| ^2) * (1. N) by A1, Def3;
A4: ||.(a *').|| = ||.a.|| by Def6;
a *' <> 0. N by A1;
hence (a *') *' = a by A2, A3, A4, ALGSTR_0:def 21, ALGSTR_0:def 37; :: thesis: verum

end;

suppose a is zero ; :: thesis: (a *') *' = a

then a = 0. N ;
hence (a *') *' = a ; :: thesis: verum

end;

end;