let n be non zero Nat; :: thesis: for c being Complex
for f being FinSequence holds (<*c*> ^ f) . (n + 1) = f . n
let c be Complex; :: thesis: for f being FinSequence holds (<*c*> ^ f) . (n + 1) = f . n
let f be FinSequence; :: thesis: (<*c*> ^ f) . (n + 1) = f . n
reconsider g = <*c*> as 1 -element FinSequence ;
len g = 1 by FINSEQ_1:40;
hence (<*c*> ^ f) . (n + 1) = f . n by FINSEQ165; :: thesis: verum