let R be non empty left_add-cancelable left_zeroed left-distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for a, b being Element of R
for n being Element of NAT holds (n * a) * b = n * (a * b)
let a, b be Element of R; :: thesis: for n being Element of NAT holds (n * a) * b = n * (a * b)
let n be Element of NAT ; :: thesis: (n * a) * b = n * (a * b)
defpred S₁[ Element of NAT ] means ($1 * a) * b = $1 * (a * b);
(0 * a) * b = (0. R) * b by Def6
.= 0. R by Th1
.= 0 * (a * b) by Def6 ;
then A1: S₁[ 0 ] ;

A2: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
((k + 1) * a) * b = (a + (k * a)) * b by Def6
.= (a * b) + (k * (a * b)) by A3, VECTSP_1:def 12
.= (1 * (a * b)) + (k * (a * b)) by Th14
.= (k + 1) * (a * b) by Th16 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2);
hence (n * a) * b = n * (a * b) ; :: thesis: verum