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
A11: 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
A12: 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
A13: len g1 = m2 by A11;
A14: 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 A15: ( 1 <= i & i <= len g1 ) ; :: thesis: g1 . i = g2 . i
then g1 . i = p . i by A11, A13;
hence g1 . i = g2 . i by A12, A13, A15; :: thesis: verum

end;

len g2 = m2 by A12;
hence g1 = g2 by A11, A14, FINSEQ_1:14; :: thesis: verum