reconsider F' = F as Element of (GFuncs the carrier of S) by MONOID_0:82;
reconsider P = Product (n |-> F') as Function of S,S by MONOID_0:82;
take P ; :: thesis: for F' being Element of (GFuncs the carrier of S) st F' = F holds
P = Product (n |-> F')
thus for F' being Element of (GFuncs the carrier of S) st F' = F holds
P = Product (n |-> F') ; :: thesis: verum