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