let L be non empty unital multMagma ; :: thesis: for x being Element of L holds FPower x,0 = the carrier of L --> x
let x be Element of L; :: thesis: FPower x,0 = the carrier of L --> x
reconsider f = the carrier of L --> x as Function of L,L ;

now

let y be Element of L; :: thesis: f . y = x * ((power L) . y,0 )
thus f . y = x by FUNCOP_1:13
.= x * (1_ L) by GROUP_1:def 5
.= x * ((power L) . y,0 ) by GROUP_1:def 8 ; :: thesis: verum

end;

hence FPower x,0 = the carrier of L --> x by Def11; :: thesis: verum