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