let p1, p2 be non empty XFinSequence 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 . 0 and
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 = 0 and
A29: len q = p2 . 0 and
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

proof

let i be Nat; :: thesis: ( i < n implies p1 . i = p2 . i )
assume i < n ; :: thesis: p1 . i = p2 . i
then A33: ( i < 0 + 1 or ( 1 <= i & i <= len q ) or ( len q < i & i < n ) ) ;

now :: thesis: ( ( i = 0 & p1 . i = p2 . i ) or ( 1 <= i & i <= len q & p1 . i = p2 . i ) or ( len q < i & i < n & p1 . i = p2 . i ) )

per cases ( i = 0 or ( 1 <= i & i <= len q ) or ( len q < i & i < n ) ) by A33, NAT_1:13;

case i = 0 ; :: thesis: p1 . i = p2 . i

hence p1 . i = p2 . i by A25, A29; :: thesis: verum

end;

case A34: ( 1 <= i & i <= len q ) ; :: thesis: p1 . i = p2 . i

then p1 . i = q . i by A27;
hence p1 . i = p2 . i by A31, A34; :: thesis: verum

end;

case A35: ( len q < i & i < n ) ; :: thesis: p1 . i = p2 . i

then p1 . i = 0 by A28;
hence p1 . i = p2 . i by A32, A35; :: thesis: verum

end;

end;

end;

hence p1 . i = p2 . i ; :: thesis: verum

end;

hence p1 = p2 by A26, A30, Th8; :: thesis: verum