let n be Nat; :: thesis: for a being Real holds n * a = n * (In (a,F_Real))
let a be Real; :: thesis: n * a = n * (In (a,F_Real))
defpred S₁[ Nat] means $1 * a = $1 * (In (a,F_Real));
0 * (In (a,F_Real)) = 0. F_Real by BINOM:12;
then A1: S₁[ 0 ] ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
reconsider a1 = a as Element of F_Real by XREAL_0:def 1;
(k + 1) * a = a1 + (k * a1) by A3
.= (1 * a1) + (k * a1) by BINOM:13 ;
hence S₁[k + 1] by BINOM:15; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence n * a = n * (In (a,F_Real)) ; :: thesis: verum