let p1, p2 be FinSequence; :: thesis: ( ( n <= len f & len p1 = (len f) - n & ( for m being Nat st m in dom p1 holds

p1 . m = f . (m + n) ) & len p2 = (len f) - n & ( for m being Nat st m in dom p2 holds

p2 . m = f . (m + n) ) implies p1 = p2 ) & ( not n <= len f & p1 = {} & p2 = {} implies p1 = p2 ) )

thus ( n <= len f & len p1 = (len f) - n & ( for m being Nat st m in dom p1 holds

p1 . m = f . (m + n) ) & len p2 = (len f) - n & ( for m being Nat st m in dom p2 holds

p2 . m = f . (m + n) ) implies p1 = p2 ) :: thesis: ( not n <= len f & p1 = {} & p2 = {} implies p1 = p2 )

p1 . m = f . (m + n) ) & len p2 = (len f) - n & ( for m being Nat st m in dom p2 holds

p2 . m = f . (m + n) ) implies p1 = p2 ) & ( not n <= len f & p1 = {} & p2 = {} implies p1 = p2 ) )

thus ( n <= len f & len p1 = (len f) - n & ( for m being Nat st m in dom p1 holds

p1 . m = f . (m + n) ) & len p2 = (len f) - n & ( for m being Nat st m in dom p2 holds

p2 . m = f . (m + n) ) implies p1 = p2 ) :: thesis: ( not n <= len f & p1 = {} & p2 = {} implies p1 = p2 )

proof

thus
( not n <= len f & p1 = {} & p2 = {} implies p1 = p2 )
; :: thesis: verum
assume that

n <= len f and

A2: len p1 = (len f) - n and

A3: for m being Nat st m in dom p1 holds

p1 . m = f . (m + n) and

A4: len p2 = (len f) - n and

A5: for m being Nat st m in dom p2 holds

p2 . m = f . (m + n) ; :: thesis: p1 = p2

A6: ( dom p1 = Seg (len p1) & Seg (len p2) = dom p2 ) by FINSEQ_1:def 3;

end;n <= len f and

A2: len p1 = (len f) - n and

A3: for m being Nat st m in dom p1 holds

p1 . m = f . (m + n) and

A4: len p2 = (len f) - n and

A5: for m being Nat st m in dom p2 holds

p2 . m = f . (m + n) ; :: thesis: p1 = p2

A6: ( dom p1 = Seg (len p1) & Seg (len p2) = dom p2 ) by FINSEQ_1:def 3;

now :: thesis: for m being Nat st m in dom p1 holds

p1 . m = p2 . m

hence
p1 = p2
by A2, A4, FINSEQ_2:9; :: thesis: verump1 . m = p2 . m

let m be Nat; :: thesis: ( m in dom p1 implies p1 . m = p2 . m )

assume A7: m in dom p1 ; :: thesis: p1 . m = p2 . m

then p1 . m = f . (m + n) by A3;

hence p1 . m = p2 . m by A2, A4, A5, A6, A7; :: thesis: verum

end;assume A7: m in dom p1 ; :: thesis: p1 . m = p2 . m

then p1 . m = f . (m + n) by A3;

hence p1 . m = p2 . m by A2, A4, A5, A6, A7; :: thesis: verum