let q, p be FinSequence; :: thesis: for n being Element of NAT st q = p | (Seg n) holds
( len q <= len p & ( for i being Element of NAT st 1 <= i & i <= len q holds
p . i = q . i ) )
let n be Element of NAT ; :: thesis: ( q = p | (Seg n) implies ( len q <= len p & ( for i being Element of NAT st 1 <= i & i <= len q holds
p . i = q . i ) ) )
assume A1: q = p | (Seg n) ; :: thesis: ( len q <= len p & ( for i being Element of NAT st 1 <= i & i <= len q holds
p . i = q . i ) )

per cases ( n <= len p or len p <= n ) ;

suppose A2: n <= len p ; :: thesis: ( len q <= len p & ( for i being Element of NAT st 1 <= i & i <= len q holds
p . i = q . i ) )

then A3: len q = n by A1, FINSEQ_1:21;
thus len q <= len p by A1, A2, FINSEQ_1:21; :: thesis: for i being Element of NAT st 1 <= i & i <= len q holds
p . i = q . i
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len q implies p . i = q . i )
assume that
A4: 1 <= i and
A5: i <= len q ; :: thesis: p . i = q . i
i in Seg n by A3, A4, A5;
hence p . i = q . i by A1, FUNCT_1:72; :: thesis: verum

end;

suppose A6: len p <= n ; :: thesis: ( len q <= len p & ( for i being Element of NAT st 1 <= i & i <= len q holds
p . i = q . i ) )

hence len q <= len p by A1, FINSEQ_2:23; :: thesis: for i being Element of NAT st 1 <= i & i <= len q holds
p . i = q . i
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len q implies p . i = q . i )
assume ( 1 <= i & i <= len q ) ; :: thesis: p . i = q . i
thus p . i = q . i by A1, A6, FINSEQ_2:23; :: thesis: verum

end;

end;