let i be Element of NAT ; :: thesis: for p being FinSequence holds dom p = dom (Seq (i Shift p))
let p be FinSequence; :: thesis: dom p = dom (Seq (i Shift p))
A1: rng (Sgm (dom (i Shift p))) = dom (i Shift p) by FINSEQ_1:71;
A2: Seq (i Shift p) = (i Shift p) * (Sgm (dom (i Shift p))) by FINSEQ_1:def 14;
A3: ( dom p = Seg (len p) & dom (Sgm (dom (i Shift p))) = Seg (len (Sgm (dom (i Shift p)))) ) by FINSEQ_1:def 3;
consider k being Nat such that
A4: dom (i Shift p) c= Seg k by FINSEQ_1:def 12;
A5: len (Sgm (dom (i Shift p))) = card (dom (i Shift p)) by A4, FINSEQ_3:44;
card (dom (i Shift p)) = card (i Shift p) by CARD_1:104;
then card (dom (i Shift p)) = len p by Th57;
hence dom p = dom (Seq (i Shift p)) by A1, A2, A3, A5, RELAT_1:46; :: thesis: verum