let p1, p2 be non emptyXFinSequence of D; :: thesis: ( len q = p1 .0 & len p1 = n & ( for i being Nat st 1 <= i & i <=len q holds p1 . i = q . i ) & ( for j being Nat st len q < j & j < n holds p1 . j =0 ) & len q = p2 .0 & len p2 = n & ( for i being Nat st 1 <= i & i <=len q holds p2 . i = q . i ) & ( for j being Nat st len q < j & j < n holds p2 . j =0 ) implies p1 = p2 ) assume that A25:
len q = p1 .0and A26:
len p1 = n
and A27:
for i being Nat st 1 <= i & i <=len q holds p1 . i = q . i
and A28:
for j being Nat st len q < j & j < n holds p1 . j =0and A29:
len q = p2 .0and A30:
len p2 = n
and A31:
for i being Nat st 1 <= i & i <=len q holds p2 . i = q . i
and A32:
for j being Nat st len q < j & j < n holds p2 . j =0
; :: thesis: p1 = p2
for i being Nat st i < n holds p1 . i = p2 . i