let L be non empty add-unital addMagma ; :: thesis: for x being Element of L holds (mult L) . (2,x) = x + x
let x be Element of L; :: thesis: (mult L) . (2,x) = x + x
1 + 1 = 2 ;
hence (mult L) . (2,x) = ((mult L) . (1,x)) + x by Def7
.= x + x by Th49 ;
:: thesis: verum