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