let i be Nat; :: thesis: exp_R . i = (power F_Real) . ((In (number_e,F_Real)),i)
reconsider x = In (number_e,F_Real) as Element of F_Real ;
defpred S₁[ Nat] means exp_R . $1 = (power F_Real) . (x,$1);
exp_R . 0 = 1_ F_Real by SIN_COS2:13;
then A1: S₁[ 0 ] by GROUP_1:def 7;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
A5: exp_R . 1 = x by IRRAT_1:def 7, SIN_COS:def 23;
(power F_Real) . (x,(k + 1)) = ((power F_Real) . (x,k)) * x by GROUP_1:def 7;
hence S₁[k + 1] by A5, A4, SIN_COS2:12; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A3);
hence exp_R . i = (power F_Real) . ((In (number_e,F_Real)),i) ; :: thesis: verum