let i be Nat; :: thesis: 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 ; :: thesis: for q being FinSubsequence st k in dom (Seq q) holds
(Seq (Shift (q,i))) . k = (Seq q) . k
let q be FinSubsequence; :: thesis: ( k in dom (Seq q) implies (Seq (Shift (q,i))) . k = (Seq q) . k )
assume A1: k in dom (Seq q) ; :: thesis: (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 ; :: thesis: verum