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