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 and
A3: (Sgm (dom (i Shift q))) . k = i + j by Th75;
A4: rng (Sgm (dom q)) = dom q by FINSEQ_1:50;
A5: dom (Seq q) = dom (Seq (i Shift q)) by Th74
.= dom ((i Shift q) * (Sgm (dom (i Shift q)))) by FINSEQ_1:def 14 ;
A6: dom (Seq q) = dom (q * (Sgm (dom q))) by FINSEQ_1:def 14
.= 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 (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, A5, FUNCT_1:12
.= q . j by A3, A7, Def15
.= (q * (Sgm (dom q))) . k by A1, A2, A6, FUNCT_1:13
.= (Seq q) . k by FINSEQ_1:def 14 ;
hence (Seq (i Shift q)) . k = (Seq q) . k ; :: thesis: verum