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