let r1, r2, r3 be real number ; :: thesis: sqr <*r1,r2,r3*> = <*(r1 ^2),(r2 ^2),(r3 ^2)*>
A1: ( r1 in REAL & r2 in REAL & r3 in REAL ) by XREAL_0:def 1;
( <*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 A1, TOPREAL6:11
.= <*(r1 ^2),(r2 ^2),(r3 ^2)*> by RVSUM_1:55 ;
:: thesis: verum