let p1, p2 be FinSequence; :: thesis: ( len p1 = len q & ( for i being Nat st 1 <= i & i <= len q holds
q . (i - 1) = p1 . i ) & len p2 = len q & ( for i being Nat st 1 <= i & i <= len q holds
q . (i - 1) = p2 . i ) implies p1 = p2 )
assume that
A12: len p1 = len q and
A13: for i being Nat st 1 <= i & i <= len q holds
q . (i - 1) = p1 . i and
A14: len p2 = len q and
A15: for i being Nat st 1 <= i & i <= len q holds
q . (i - 1) = p2 . i ; :: thesis: p1 = p2
for i being Nat st 1 <= i & i <= len p1 holds
p1 . i = p2 . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len p1 implies p1 . i = p2 . i )
assume A16: ( 1 <= i & i <= len p1 ) ; :: thesis: p1 . i = p2 . i
then q . (i - 1) = p1 . i by A12, A13;
hence p1 . i = p2 . i by A12, A15, A16; :: thesis: verum

end;

hence p1 = p2 by A12, A14, FINSEQ_1:14; :: thesis: verum