reconsider m2 = p . 0 as Nat by A1;
let g1, g2 be FinSequence of D; :: thesis: ( ( for m being Nat st m = p . 0 holds
( len g1 = m & ( for i being Nat st 1 <= i & i <= m holds
g1 . i = p . i ) ) ) & ( for m being Nat st m = p . 0 holds
( len g2 = m & ( for i being Nat st 1 <= i & i <= m holds
g2 . i = p . i ) ) ) implies g1 = g2 )
assume that
A10: for m being Nat st m = p . 0 holds
( len g1 = m & ( for i being Nat st 1 <= i & i <= m holds
g1 . i = p . i ) ) and
A11: for m being Nat st m = p . 0 holds
( len g2 = m & ( for i being Nat st 1 <= i & i <= m holds
g2 . i = p . i ) ) ; :: thesis: g1 = g2
A12: len g1 = m2 by A10;
A13: for i being Nat st 1 <= i & i <= len g1 holds
g1 . i = g2 . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len g1 implies g1 . i = g2 . i )
assume A14: ( 1 <= i & i <= len g1 ) ; :: thesis: g1 . i = g2 . i
then g1 . i = p . i by A10, A12;
hence g1 . i = g2 . i by A11, A12, A14; :: thesis: verum

end;

len g2 = m2 by A11;
hence g1 = g2 by A10, A13, FINSEQ_1:14; :: thesis: verum