let S be 1-sorted ; :: thesis: for F being Function of S,S holds F |^ 0 = id S
let F be Function of S,S; :: thesis: F |^ 0 = id S
set G = GFuncs the carrier of S;
reconsider F9 = F as Element of (GFuncs the carrier of S) by MONOID_0:73;
0 |-> F9 = <*> the carrier of (GFuncs the carrier of S) ;
then Product (0 |-> F9) = 1_ (GFuncs the carrier of S) by GROUP_4:8
.= the_unity_wrt the multF of (GFuncs the carrier of S) by GROUP_1:22
.= id S by MONOID_0:75 ;
hence F |^ 0 = id S by Def4; :: thesis: verum