let k, i be Element of NAT ; :: thesis: for q being FinSubsequence st k in dom (Seq q) holds
(Seq (i Shift q)) . k = (Seq q) . k
let q be FinSubsequence; :: thesis: ( k in dom (Seq q) implies (Seq (i Shift q)) . k = (Seq q) . k )
assume A1: k in dom (Seq q) ; :: thesis: (Seq (i Shift q)) . k = (Seq q) . k
then consider j being Element of NAT such that
A2: ( j = (Sgm (dom q)) . k & (Sgm (dom (i Shift q))) . k = i + j ) by Th75;
A3: ( rng (Sgm (dom q)) = dom q & rng (Sgm (dom (i Shift q))) = dom (i Shift q) ) by FINSEQ_1:71;
A4: dom (Seq q) = dom (Seq (i Shift q)) by Th74
.= dom ((i Shift q) * (Sgm (dom (i Shift q)))) by FINSEQ_1:def 14 ;
A5: dom (Seq q) = dom (q * (Sgm (dom q))) by FINSEQ_1:def 14
.= dom (Sgm (dom q)) by A3, RELAT_1:46 ;
then j in rng (Sgm (dom q)) by A1, A2, FUNCT_1:def 5;
then A6: j in dom q by FINSEQ_1:71;
(Seq (i Shift q)) . k = ((i Shift q) * (Sgm (dom (i Shift q)))) . k by FINSEQ_1:def 14
.= (i Shift q) . ((Sgm (dom (i Shift q))) . k) by A1, A4, FUNCT_1:22
.= q . j by A2, A6, Def15
.= (q * (Sgm (dom q))) . k by A1, A2, A5, FUNCT_1:23
.= (Seq q) . k by FINSEQ_1:def 14 ;
hence (Seq (i Shift q)) . k = (Seq q) . k ; :: thesis: verum