let n be Nat; :: thesis: for z being Element of INT.Ring
for r being Real st z = r holds
n * z = n * r
let z be Element of INT.Ring; :: thesis: for r being Real st z = r holds
n * z = n * r
let r be Real; :: thesis: ( z = r implies n * z = n * r )
assume A1: z = r ; :: thesis: n * z = n * r
defpred S₁[ Nat] means $1 * z = $1 * r;
0 * z = 0. INT.Ring by BINOM:12;
then A2: S₁[ 0 ] ;
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]
(k + 1) * z = (k * z) + (1 * z) by BINOM:15
.= (k * r) + r by A1, A4, BINOM:13
.= (k + 1) * r ;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A3);
hence n * z = n * r ; :: thesis: verum