let p, q be XFinSequence; :: thesis: ( len p = len q & ( for k being Nat st k < len p holds
p . k = q . k ) implies p = q )
assume that
A1: len p = len q and
A2: for k being Nat st k < len p holds
p . k = q . k ; :: thesis: p = q
for x being object st x in dom p holds
p . x = q . x by A2, Lm1;
hence p = q by A1; :: thesis: verum