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