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 F9 = F as Element of (GFuncs the carrier of S) by MONOID_0:73;
Product (1 |-> F9) = Product <*F9*> by FINSEQ_2:59
.= F9 by GROUP_4:9 ;
hence F |^ 1 = F by Def4; :: thesis: verum