let p, q be FinSequence; :: thesis: for n being Nat st q = p | (Seg n) holds

( len q <= len p & ( for i being Nat st 1 <= i & i <= len q holds

p . i = q . i ) )

let n be Nat; :: thesis: ( q = p | (Seg n) implies ( len q <= len p & ( for i being 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 Nat st 1 <= i & i <= len q holds

p . i = q . i ) )

( len q <= len p & ( for i being Nat st 1 <= i & i <= len q holds

p . i = q . i ) )

let n be Nat; :: thesis: ( q = p | (Seg n) implies ( len q <= len p & ( for i being 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 Nat st 1 <= i & i <= len q holds

p . i = q . i ) )

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

end;

suppose A2:
n <= len p
; :: thesis: ( len q <= len p & ( for i being Nat st 1 <= i & i <= len q holds

p . i = q . i ) )

p . i = q . i ) )

hence
len q <= len p
by A1, FINSEQ_1:17; :: thesis: for i being Nat st 1 <= i & i <= len q holds

p . i = q . i

let i be Nat; :: thesis: ( 1 <= i & i <= len q implies p . i = q . i )

assume that

A3: 1 <= i and

A4: i <= len q ; :: thesis: p . i = q . i

len q = n by A1, A2, FINSEQ_1:17;

then i in Seg n by A3, A4;

hence p . i = q . i by A1, FUNCT_1:49; :: thesis: verum

end;p . i = q . i

let i be Nat; :: thesis: ( 1 <= i & i <= len q implies p . i = q . i )

assume that

A3: 1 <= i and

A4: i <= len q ; :: thesis: p . i = q . i

len q = n by A1, A2, FINSEQ_1:17;

then i in Seg n by A3, A4;

hence p . i = q . i by A1, FUNCT_1:49; :: thesis: verum

suppose A5:
len p <= n
; :: thesis: ( len q <= len p & ( for i being Nat st 1 <= i & i <= len q holds

p . i = q . i ) )

p . i = q . i ) )

hence
len q <= len p
by A1, FINSEQ_2:20; :: thesis: for i being Nat st 1 <= i & i <= len q holds

p . i = q . i

let i be Nat; :: thesis: ( 1 <= i & i <= len q implies p . i = q . i )

assume that

1 <= i and

i <= len q ; :: thesis: p . i = q . i

thus p . i = q . i by A1, A5, FINSEQ_2:20; :: thesis: verum

end;p . i = q . i

let i be Nat; :: thesis: ( 1 <= i & i <= len q implies p . i = q . i )

assume that

1 <= i and

i <= len q ; :: thesis: p . i = q . i

thus p . i = q . i by A1, A5, FINSEQ_2:20; :: thesis: verum