let n be Nat; :: thesis: for G being addGroup
for h being Element of G holds
( (n + 1) * h = (n * h) + h & (n + 1) * h = h + (n * h) )
let G be addGroup; :: thesis: for h being Element of G holds
( (n + 1) * h = (n * h) + h & (n + 1) * h = h + (n * h) )
let h be Element of G; :: thesis: ( (n + 1) * h = (n * h) + h & (n + 1) * h = h + (n * h) )
thus (n + 1) * h = (n * h) + h by Def7; :: thesis: (n + 1) * h = h + (n * h)
thus (n + 1) * h = (1 * h) + (n * h) by Lm5
.= h + (n * h) by Th25 ; :: thesis: verum