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