reconsider F' = F as Element of 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 st F' = F holds
P = Product (n |-> F')
thus for F' being Element of st F' = F holds
P = Product (n |-> F') ; :: thesis: verum