let L be non empty Abelian add-associative add-unital addMagma ; :: thesis: for x, y being Element of L
for n being Nat holds (mult L) . (n,(x + y)) = ((mult L) . (n,x)) + ((mult L) . (n,y))
let x, y be Element of L; :: thesis: for n being Nat holds (mult L) . (n,(x + y)) = ((mult L) . (n,x)) + ((mult L) . (n,y))
defpred S₁[ Nat] means (mult L) . ($1,(x + y)) = ((mult L) . ($1,x)) + ((mult L) . ($1,y));

A1: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then (mult L) . ((n + 1),(x + y)) = (((mult L) . (n,x)) + ((mult L) . (n,y))) + (x + y) by Def7
.= ((mult L) . (n,x)) + (((mult L) . (n,y)) + (x + y)) by RLVECT_1:def 3
.= ((mult L) . (n,x)) + (x + (((mult L) . (n,y)) + y)) by RLVECT_1:def 3
.= ((mult L) . (n,x)) + (x + ((mult L) . ((n + 1),y))) by Def7
.= (((mult L) . (n,x)) + x) + ((mult L) . ((n + 1),y)) by RLVECT_1:def 3
.= ((mult L) . ((n + 1),x)) + ((mult L) . ((n + 1),y)) by Def7 ;
hence S₁[n + 1] ; :: thesis: verum

end;

(mult L) . (0,(x + y)) = 0_ L by Def7
.= (0_ L) + (0_ L) by Def4
.= ((mult L) . (0,x)) + (0_ L) by Def7
.= ((mult L) . (0,x)) + ((mult L) . (0,y)) by Def7 ;
then A2: S₁[ 0 ] ;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A1); :: thesis: verum