let seq be Complex_Sequence; :: thesis: for Nseq being increasing sequence of NAT
for n being Nat holds (seq * Nseq) . n = seq . (Nseq . n)
let Nseq be increasing sequence of NAT; :: thesis: for n being Nat holds (seq * Nseq) . n = seq . (Nseq . n)
let n be Nat; :: thesis: (seq * Nseq) . n = seq . (Nseq . n)
A1: n in NAT by ORDINAL1:def 12;
dom (seq * Nseq) = NAT by FUNCT_2:def 1;
hence (seq * Nseq) . n = seq . (Nseq . n) by FUNCT_1:12, A1; :: thesis: verum