reconsider F9 = F as Element of (GFuncs the carrier of S) by MONOID_0:73;
let F1, F2 be Function of S,S; :: thesis: ( ( for F9 being Element of (GFuncs the carrier of S) st F9 = F holds
F1 = Product (n |-> F9) ) & ( for F9 being Element of (GFuncs the carrier of S) st F9 = F holds
F2 = Product (n |-> F9) ) implies F1 = F2 )
assume that
A1: for F9 being Element of (GFuncs the carrier of S) st F9 = F holds
F1 = Product (n |-> F9) and
A2: for F9 being Element of (GFuncs the carrier of S) st F9 = F holds
F2 = Product (n |-> F9) ; :: thesis: F1 = F2
thus F1 = Product (n |-> F9) by A1
.= F2 by A2 ; :: thesis: verum