let r1, r2, r3 be Real; sqr <*r1,r2,r3*> = <*(r1 ^2),(r2 ^2),(r3 ^2)*>
( <*r1,r2*> is FinSequence of REAL & <*r3*> is FinSequence of REAL )
by TOPREALC:19;
hence sqr <*r1,r2,r3*> =
(sqr <*r1,r2*>) ^ (sqr <*r3*>)
by TOPREAL7:10
.=
<*(r1 ^2),(r2 ^2)*> ^ (sqr <*r3*>)
by TOPREAL6:11
.=
<*(r1 ^2),(r2 ^2),(r3 ^2)*>
by RVSUM_1:55
;
verum