let p1, p2 be non empty XFinSequence of ; :: 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 A23: ( 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 ) ) ; :: thesis: p1 = p2
for i being Element of NAT st i < n holds
p1 . i = p2 . i

proof

let i be Element of NAT ; :: thesis: ( i < n implies p1 . i = p2 . i )
assume A24: i < n ; :: thesis: p1 . i = p2 . i
( i < 0 + 1 or ( 1 <= i & i <= len q ) or ( len q < i & i < n ) ) by A24;
then A25: ( i <= 0 or ( 1 <= i & i <= len q ) or ( len q < i & i < n ) ) by NAT_1:13;

now

per cases ( i = 0 or ( 1 <= i & i <= len q ) or ( len q < i & i < n ) ) by A25;

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

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

end;

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

then p1 . i = q . i by A23;
hence p1 . i = p2 . i by A23, A26; :: thesis: verum

end;

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

then p1 . i = 0 by A23;
hence p1 . i = p2 . i by A23, A27; :: thesis: verum

end;

end;

end;

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

end;

hence p1 = p2 by A23, AFINSQ_1:11; :: thesis: verum