let i be natural Number ; :: thesis: for r being Real holds sqr (i |-> r) = i |-> (r ^2)
let r be Real; :: thesis: sqr (i |-> r) = i |-> (r ^2)
reconsider s = r as Element of REAL by XREAL_0:def 1;
sqr (i |-> s) = i |-> (sqrreal . s) by FINSEQOP:16
.= i |-> (r ^2) by Def2 ;
hence sqr (i |-> r) = i |-> (r ^2) ; :: thesis: verum