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