let i be Nat; for k being Element of NAT
for q being FinSubsequence st k in dom (Seq q) holds
(Seq (Shift (q,i))) . k = (Seq q) . k
let k be Element of NAT ; for q being FinSubsequence st k in dom (Seq q) holds
(Seq (Shift (q,i))) . k = (Seq q) . k
let q be FinSubsequence; ( k in dom (Seq q) implies (Seq (Shift (q,i))) . k = (Seq q) . k )
assume A1:
k in dom (Seq q)
; (Seq (Shift (q,i))) . k = (Seq q) . k
then consider j being Element of NAT such that
A2:
j = (Sgm (dom q)) . k
and
A3:
(Sgm (dom (Shift (q,i)))) . k = i + j
by Th56;
A4:
rng (Sgm (dom q)) = dom q
by FINSEQ_1:50;
A5: dom (Seq q) =
dom (Seq (Shift (q,i)))
by Th55
.=
dom ((Shift (q,i)) * (Sgm (dom (Shift (q,i)))))
;
A6: dom (Seq q) =
dom (q * (Sgm (dom q)))
.=
dom (Sgm (dom q))
by A4, RELAT_1:27
;
then
j in rng (Sgm (dom q))
by A1, A2, FUNCT_1:def 3;
then A7:
j in dom q
by FINSEQ_1:50;
(Seq (Shift (q,i))) . k =
((Shift (q,i)) * (Sgm (dom (Shift (q,i))))) . k
.=
(Shift (q,i)) . ((Sgm (dom (Shift (q,i)))) . k)
by A1, A5, FUNCT_1:12
.=
q . j
by A3, A7, Def12
.=
(q * (Sgm (dom q))) . k
by A1, A2, A6, FUNCT_1:13
.=
(Seq q) . k
;
hence
(Seq (Shift (q,i))) . k = (Seq q) . k
; verum