let i be Integer; :: thesis: for G being addGroup
for h being Element of G holds
( (i + 1) * h = (i * h) + h & (i + 1) * h = h + (i * h) )
let G be addGroup; :: thesis: for h being Element of G holds
( (i + 1) * h = (i * h) + h & (i + 1) * h = h + (i * h) )
let h be Element of G; :: thesis: ( (i + 1) * h = (i * h) + h & (i + 1) * h = h + (i * h) )
1 * h = h by Th25;
hence ( (i + 1) * h = (i * h) + h & (i + 1) * h = h + (i * h) ) by Th32; :: thesis: verum