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 Def8
.= x * x by Th98 ;
:: thesis: verum