let i be Nat; :: thesis: for k being Element of NAT
for p being FinSequence st k in dom p holds
(Seq (Shift (p,i))) . k = p . k
let k be Element of NAT ; :: thesis: for p being FinSequence st k in dom p holds
(Seq (Shift (p,i))) . k = p . k
let p be FinSequence; :: thesis: ( k in dom p implies (Seq (Shift (p,i))) . k = p . k )
assume A1: k in dom p ; :: thesis: (Seq (Shift (p,i))) . k = p . k
then A2: k in dom (Seq (Shift (p,i))) by Th42;
((Shift (p,i)) * (Sgm (dom (Shift (p,i))))) . k = (Shift (p,i)) . ((Sgm (dom (Shift (p,i)))) . k) by A2, FUNCT_1:12
.= (Shift (p,i)) . (i + k) by A1, Th43 ;
hence (Seq (Shift (p,i))) . k = p . k by A1, Def12; :: thesis: verum