let r be Real; :: thesis: sqr <*r*> = <*(r ^2)*>
reconsider s = r as Element of REAL by XREAL_0:def 1;
sqr <*s*> = <*(sqrreal . s)*> by FINSEQ_2:35
.= <*(r ^2)*> by Def2 ;
hence sqr <*r*> = <*(r ^2)*> ; :: thesis: verum