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 :: thesis: for y being Element of L holds f . y = x * (power (y,0))
let y be Element of L; :: thesis: f . y = x * (power (y,0))
thus f . y = x by FUNCOP_1:7
.= x * (1_ L) by GROUP_1:def 4
.= x * (power (y,0)) by GROUP_1:def 7 ; :: thesis: verum
end;
hence FPower (x,0) = the carrier of L --> x by Def12; :: thesis: verum