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 ) )

per cases ( n <= len p or len p <= n ) ;
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 ) )

hence len q <= len p by ; :: 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 ;
then i in Seg n by A3, A4;
hence p . i = q . i by ; :: thesis: verum
end;
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 ) )

hence len q <= len p by ; :: 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 ; :: thesis: verum
end;
end;