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