let L be non empty Abelian add-associative add-unital addMagma ; 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; for n being Nat holds (mult L) . (n,(x + y)) = ((mult L) . (n,x)) + ((mult L) . (n,y))
defpred S1[ Nat] means (mult L) . ($1,(x + y)) = ((mult L) . ($1,x)) + ((mult L) . ($1,y));
A1:
now for n being Nat st S1[n] holds
S1[n + 1]let n be
Nat;
( S1[n] implies S1[n + 1] )assume
S1[
n]
;
S1[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
S1[
n + 1]
;
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:
S1[ 0 ]
;
thus
for n being Nat holds S1[n]
from NAT_1:sch 2(A2, A1); verum