let i be Nat; :: thesis: for p being FinSequence ex fs being FinSequence st
( dom fs = dom p & rng fs = dom (Shift (p,i)) & ( 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 (Shift (p,i)) & ( 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 and
A2: rng ss = dom (Shift (p,i)) and
A3: for k being Element of NAT st k in dom p holds
ss . k = i + k and
A4: ss is one-to-one by Th40;
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 by A1;
hence ex fs being FinSequence st
( dom fs = dom p & rng fs = dom (Shift (p,i)) & ( for k being Element of NAT st k in dom p holds
fs . k = i + k ) & fs is one-to-one ) by A2, A3, A4; :: thesis: verum