let R be domRing; :: thesis: for n, m being Nat
for b being Element of R holds (n * m) * b = n * (m * b)
let n, m be Nat; :: thesis: for b being Element of R holds (n * m) * b = n * (m * b)
let b be Element of R; :: thesis: (n * m) * b = n * (m * b)
defpred S₁[ Nat] means ($1 * m) * b = $1 * (m * b);
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
((n + 1) * m) * b = ((n * m) + (1 * m)) * b
.= ((n * m) * b) + (m * b) by BINOM:15
.= (n * (m * b)) + (1 * (m * b)) by A2, BINOM:13
.= (n + 1) * (m * b) by BINOM:15 ;
hence S₁[n + 1] ; :: thesis: verum

end;

(0 * m) * b = 0. R by BINOM:12
.= 0 * (m * b) by BINOM:12 ;
then A3: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1);
hence (n * m) * b = n * (m * b) ; :: thesis: verum