let R be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for a, b being Element of R
for i being Element of NAT holds (Nat-mult-left R) . (i,(a + b)) = ((Nat-mult-left R) . (i,a)) + ((Nat-mult-left R) . (i,b))
let a, b be Element of R; :: thesis: for i being Element of NAT holds (Nat-mult-left R) . (i,(a + b)) = ((Nat-mult-left R) . (i,a)) + ((Nat-mult-left R) . (i,b))
let i be Element of NAT ; :: thesis: (Nat-mult-left R) . (i,(a + b)) = ((Nat-mult-left R) . (i,a)) + ((Nat-mult-left R) . (i,b))
defpred S₁[ Element of NAT ] means (Nat-mult-left R) . ($1,(a + b)) = ((Nat-mult-left R) . ($1,a)) + ((Nat-mult-left R) . ($1,b));
A1: S₁[ 0 ]

proof

(Nat-mult-left R) . (0,(a + b)) = 0. R by BINOM:def 3
.= (0. R) + (0. R) by RLVECT_1:4
.= ((Nat-mult-left R) . (0,a)) + (0. R) by BINOM:def 3
.= ((Nat-mult-left R) . (0,a)) + ((Nat-mult-left R) . (0,b)) by BINOM:def 3 ;
hence S₁[ 0 ] ; :: thesis: verum

end;

A2: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
(Nat-mult-left R) . ((n + 1),(a + b)) = (a + b) + ((Nat-mult-left R) . (n,(a + b))) by BINOM:def 3
.= ((a + b) + ((Nat-mult-left R) . (n,a))) + ((Nat-mult-left R) . (n,b)) by A3, RLVECT_1:def 3
.= ((a + ((Nat-mult-left R) . (n,a))) + b) + ((Nat-mult-left R) . (n,b)) by RLVECT_1:def 3
.= (((Nat-mult-left R) . ((n + 1),a)) + b) + ((Nat-mult-left R) . (n,b)) by BINOM:def 3
.= ((Nat-mult-left R) . ((n + 1),a)) + (b + ((Nat-mult-left R) . (n,b))) by RLVECT_1:def 3
.= ((Nat-mult-left R) . ((n + 1),a)) + ((Nat-mult-left R) . ((n + 1),b)) by BINOM:def 3 ;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2);
hence (Nat-mult-left R) . (i,(a + b)) = ((Nat-mult-left R) . (i,a)) + ((Nat-mult-left R) . (i,b)) ; :: thesis: verum