let seq be Complex_Sequence; :: thesis: for Ns being V42() sequence of NAT holds
( (- seq) * Ns = - (seq * Ns) & |.seq.| * Ns = |.(seq * Ns).| )
let Ns be V42() sequence of NAT; :: thesis: ( (- seq) * Ns = - (seq * Ns) & |.seq.| * Ns = |.(seq * Ns).| )
thus (- seq) * Ns = ((- 1r) (#) seq) * Ns by COMSEQ_1:11
.= (- 1r) (#) (seq * Ns) by Th3
.= - (seq * Ns) by COMSEQ_1:11 ; :: thesis: |.seq.| * Ns = |.(seq * Ns).|
now :: thesis: for n being Element of NAT holds (|.seq.| * Ns) . n = |.(seq * Ns).| . n
let n be Element of NAT ; :: thesis: (|.seq.| * Ns) . n = |.(seq * Ns).| . n
thus (|.seq.| * Ns) . n = |.seq.| . (Ns . n) by FUNCT_2:15
.= |.(seq . (Ns . n)).| by VALUED_1:18
.= |.((seq * Ns) . n).| by FUNCT_2:15
.= |.(seq * Ns).| . n by VALUED_1:18 ; :: thesis: verum
end;
hence |.seq.| * Ns = |.(seq * Ns).| by FUNCT_2:63; :: thesis: verum