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:82;
0 |-> F9 = <*> the carrier of (GFuncs the carrier of S) ;
then Product (0 |-> F9) = 1_ (GFuncs the carrier of S) by GROUP_4:11
.= the_unity_wrt the multF of (GFuncs the carrier of S) by GROUP_1:33
.= id S by MONOID_0:84 ;
hence F |^ 0 = id S by Def4; :: thesis: verum