let i be Nat; :: thesis: for r being real number holds sqr (i |-> r) = i |-> (r ^2)
let r be real number ; :: 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