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:17
.= i |-> (r ^2 ) by Def2 ;
hence sqr (i |-> r) = i |-> (r ^2 ) ; :: thesis: verum