let L be non empty unital multMagma ; :: thesis: FPower ((1_ L),1) = id the carrier of L
A1: now :: thesis: for x being object st x in the carrier of L holds
(FPower ((1_ L),1)) . x = x
let x be object ; :: 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 (x1,1)) by Def12
.= (power L) . (x1,1) by GROUP_1:def 4 ;
hence (FPower ((1_ L),1)) . x = x by GROUP_1:50; :: thesis: verum
end;
dom (FPower ((1_ L),1)) = the carrier of L by FUNCT_2:def 1;
hence FPower ((1_ L),1) = id the carrier of L by A1, FUNCT_1:17; :: thesis: verum