let D be non empty set ; :: thesis: for f, g being FinSequence of D st ( for n being Nat holds f | n = g | n ) holds
f = g
let f, g be FinSequence of D; :: thesis: ( ( for n being Nat holds f | n = g | n ) implies f = g )
assume A1: for n being Nat holds f | n = g | n ; :: thesis: f = g

A2: now :: thesis: not len f <> len g

assume A3: len f <> len g ; :: thesis: contradiction

per cases ( len f < len g or len g < len f ) by A3, XXREAL_0:1;

suppose A4: len f < len g ; :: thesis: contradiction

A5: g | (len g) = g by FINSEQ_1:58;
f | (len g) = f by A4, FINSEQ_1:58;
hence contradiction by A1, A4, A5; :: thesis: verum

end;

suppose A6: len g < len f ; :: thesis: contradiction

then ( f | (len f) = f & g | (len f) = g ) by FINSEQ_1:58;
hence contradiction by A1, A6; :: thesis: verum

end;

end;

end;

( f | (len f) = f & g | (len g) = g ) by FINSEQ_1:58;
hence f = g by A1, A2; :: thesis: verum