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 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;
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 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;
end;