let i, j be Integer; :: thesis: for G being addGroup
for h being Element of G holds (i + j) * h = (i * h) + (j * h)
let G be addGroup; :: thesis: for h being Element of G holds (i + j) * h = (i * h) + (j * h)
let h be Element of G; :: thesis: (i + j) * h = (i * h) + (j * h)
defpred S₁[ Integer] means for i being Integer holds (i + $1) * h = (i * h) + ($1 * h);
A1: for j being Integer st S₁[j] holds
( S₁[j - 1] & S₁[j + 1] )

proof

let j be Integer; :: thesis: ( S₁[j] implies ( S₁[j - 1] & S₁[j + 1] ) )
assume A2: for i being Integer holds (i + j) * h = (i * h) + (j * h) ; :: thesis: ( S₁[j - 1] & S₁[j + 1] )
thus for i being Integer holds (i + (j - 1)) * h = (i * h) + ((j - 1) * h) :: thesis: S₁[j + 1]

proof

let i be Integer; :: thesis: (i + (j - 1)) * h = (i * h) + ((j - 1) * h)
thus (i + (j - 1)) * h = ((i - 1) + j) * h
.= ((i - 1) * h) + (j * h) by A2
.= ((i * h) + ((- 1) * h)) + (j * h) by Lm14
.= (i * h) + (((- 1) * h) + (j * h)) by RLVECT_1:def 3
.= (i * h) + ((j + (- 1)) * h) by A2
.= (i * h) + ((j - 1) * h) ; :: thesis: verum

end;

let i be Integer; :: thesis: (i + (j + 1)) * h = (i * h) + ((j + 1) * h)
thus (i + (j + 1)) * h = ((i + 1) + j) * h
.= ((i + 1) * h) + (j * h) by A2
.= ((i * h) + (1 * h)) + (j * h) by Lm16
.= (i * h) + ((1 * h) + (j * h)) by RLVECT_1:def 3
.= (i * h) + ((j + 1) * h) by A2 ; :: thesis: verum

end;

A3: S₁[ 0 ]

proof

let i be Integer; :: thesis: (i + 0) * h = (i * h) + (0 * h)
thus (i + 0) * h = (i * h) + (0_ G) by Def4
.= (i * h) + (0 * h) by Def7 ; :: thesis: verum

end;

for j being Integer holds S₁[j] from INT_1:sch 4(A3, A1);
hence (i + j) * h = (i * h) + (j * h) ; :: thesis: verum