let i be Nat; for p being FinSequence holds dom p = dom (Seq (Shift (p,i)))
let p be FinSequence; 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; verum