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