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

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