let seq be Complex_Sequence; :: thesis: for Nseq being V32() sequence of NAT
for n being Element of NAT holds (seq * Nseq) . n = seq . (Nseq . n)
let Nseq be V32() sequence of NAT ; :: thesis: for n being Element of NAT holds (seq * Nseq) . n = seq . (Nseq . n)
let n be Element of NAT ; :: thesis: (seq * Nseq) . n = seq . (Nseq . n)
dom (seq * Nseq) = NAT by FUNCT_2:def 1;
hence (seq * Nseq) . n = seq . (Nseq . n) by FUNCT_1:22; :: thesis: verum