let L be non empty unital multMagma ; :: thesis: FPower (1_ L),1 = id the carrier of L
A1: dom (FPower (1_ L),1) = the carrier of L by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in the carrier of L implies (FPower (1_ L),1) . x = x )
assume x in the carrier of L ; :: thesis: (FPower (1_ L),1) . x = x
then reconsider x1 = x as Element of L ;
(FPower (1_ L),1) . x1 = (1_ L) * ((power L) . x1,1) by Def11
.= (power L) . x1,1 by GROUP_1:def 5 ;
hence (FPower (1_ L),1) . x = x by GROUP_1:98; :: thesis: verum

end;

hence FPower (1_ L),1 = id the carrier of L by A1, FUNCT_1:34; :: thesis: verum