let S be 1-sorted ; :: thesis: for F being Function of S,S holds F |^ 1 = F
let F be Function of S,S; :: thesis: F |^ 1 = F
set G = GFuncs the carrier of S;
reconsider F' = F as Element of by MONOID_0:82;
Product (1 |-> F') = Product <*F'*> by FINSEQ_2:73
.= F' by GROUP_4:12 ;
hence F |^ 1 = F by Def4; :: thesis: verum