let i be Nat; :: thesis: for p being FinSequence holds dom p = dom (Seq (Shift (p,i)))
let p be FinSequence; :: thesis: dom p = dom (Seq (Shift (p,i)))
A1: rng (Sgm (dom (Shift (p,i)))) = dom (Shift (p,i)) by FINSEQ_1:50;
A2: dom p = Seg (len p) by FINSEQ_1:def 3;
A3: dom (Sgm (dom (Shift (p,i)))) = Seg (len (Sgm (dom (Shift (p,i))))) by FINSEQ_1:def 3;
ex k being Nat st dom (Shift (p,i)) c= Seg k by FINSEQ_1:def 12;
then A4: len (Sgm (dom (Shift (p,i)))) = card (dom (Shift (p,i))) by FINSEQ_3:39;
card (dom (Shift (p,i))) = card (Shift (p,i)) by CARD_1:62;
then card (dom (Shift (p,i))) = len p by Th41;
hence dom p = dom (Seq (Shift (p,i))) by A1, A2, A3, A4, RELAT_1:27; :: thesis: verum