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