for t1, t2 being sequence of S st ( for n being Nat holds t1 . n = t . (n + k) ) & ( for n being Nat holds t2 . n = t . (n + k) ) holds
t1 = t2

proof

let t1, t2 be sequence of S; :: thesis: ( ( for n being Nat holds t1 . n = t . (n + k) ) & ( for n being Nat holds t2 . n = t . (n + k) ) implies t1 = t2 )
assume that
A5: for n being Nat holds t1 . n = t . (n + k) and
A6: for n being Nat holds t2 . n = t . (n + k) ; :: thesis: t1 = t2
for x being set st x in NAT holds
t1 . x = t2 . x

proof

let x be set ; :: thesis: ( x in NAT implies t1 . x = t2 . x )
assume A7: x in NAT ; :: thesis: t1 . x = t2 . x
reconsider x = x as Nat by A7;
t1 . x = t . (x + k) by A5
.= t2 . x by A6 ;
hence t1 . x = t2 . x ; :: thesis: verum

end;

hence t1 = t2 by FUNCT_2:18; :: thesis: verum

end;

hence for b₁, b₂ being sequence of S st ( for n being Nat holds b₁ . n = t . (n + k) ) & ( for n being Nat holds b₂ . n = t . (n + k) ) holds
b₁ = b₂ ; :: thesis: verum