let i be Element of NAT ; :: thesis: for p being FinSequence ex fs being FinSequence st
( dom fs = dom p & rng fs = dom (i Shift p) & ( for k being Element of NAT st k in dom p holds
fs . k = i + k ) & fs is one-to-one )
let p be FinSequence; :: thesis: ex fs being FinSequence st
( dom fs = dom p & rng fs = dom (i Shift p) & ( for k being Element of NAT st k in dom p holds
fs . k = i + k ) & fs is one-to-one )
consider ss being FinSubsequence such that
A1: ( dom ss = dom p & rng ss = dom (i Shift p) & ( for k being Element of NAT st k in dom p holds
ss . k = i + k ) & ss is one-to-one ) by Th56;
dom ss = Seg (len p) by A1, FINSEQ_1:def 3;
then reconsider fs = ss as FinSequence by FINSEQ_1:def 2;
( dom fs = dom p & rng fs = dom (i Shift p) & ( for k being Element of NAT st k in dom p holds
fs . k = i + k ) & fs is one-to-one ) by A1;
hence ex fs being FinSequence st
( dom fs = dom p & rng fs = dom (i Shift p) & ( for k being Element of NAT st k in dom p holds
fs . k = i + k ) & fs is one-to-one ) ; :: thesis: verum