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:50;
A2: Seq (i Shift p) = (i Shift p) * (Sgm (dom (i Shift p))) by FINSEQ_1:def 14;
A3: dom p = Seg (len p) by FINSEQ_1:def 3;
A4: dom (Sgm (dom (i Shift p))) = Seg (len (Sgm (dom (i Shift p)))) by FINSEQ_1:def 3;
ex k being Nat st dom (i Shift p) c= Seg k by FINSEQ_1:def 12;
then A5: len (Sgm (dom (i Shift p))) = card (dom (i Shift p)) by FINSEQ_3:39;
card (dom (i Shift p)) = card (i Shift p) by CARD_1:62;
then card (dom (i Shift p)) = len p by Th57;
hence dom p = dom (Seq (i Shift p)) by A1, A2, A3, A4, A5, RELAT_1:27; :: thesis: verum