let c1, c2 be Complex; :: thesis: <*c1,c2*> ^2 = <*(c1 ^2),(c2 ^2)*>
( <*c1*> ^2 = <*(c1 ^2)*> & <*c2*> ^2 = <*(c2 ^2)*> ) by Th7;
hence <*c1,c2*> ^2 = <*(c1 ^2),(c2 ^2)*> by NUMBER15:59; :: thesis: verum