set j = the Element of J;
let X, Y be FinSequence of NAT ; :: thesis: ( ( for j being Element of J holds X = signature (A . j) ) & ( for j being Element of J holds Y = signature (A . j) ) implies X = Y )
assume that
A1: for j being Element of J holds X = signature (A . j) and
A2: for j being Element of J holds Y = signature (A . j) ; :: thesis: X = Y
reconsider U0 = A . the Element of J as Universal_Algebra ;
X = signature U0 by A1;
hence X = Y by A2; :: thesis: verum