let seq be Real_Sequence; :: thesis: for Ns being V33() sequence of NAT holds
( (- seq) * Ns = - (seq * Ns) & (abs seq) * Ns = abs (seq * Ns) )
let Ns be V33() sequence of NAT; :: thesis: ( (- seq) * Ns = - (seq * Ns) & (abs seq) * Ns = abs (seq * Ns) )
thus (- seq) * Ns = ((- 1) (#) seq) * Ns
.= (- 1) (#) (seq * Ns) by Th14
.= - (seq * Ns) ; :: thesis: (abs seq) * Ns = abs (seq * Ns)

now

let n be Element of NAT ; :: thesis: ((abs seq) * Ns) . n = (abs (seq * Ns)) . n
thus ((abs seq) * Ns) . n = (abs seq) . (Ns . n) by FUNCT_2:15
.= abs (seq . (Ns . n)) by SEQ_1:12
.= abs ((seq * Ns) . n) by FUNCT_2:15
.= (abs (seq * Ns)) . n by SEQ_1:12 ; :: thesis: verum

end;

hence (abs seq) * Ns = abs (seq * Ns) by FUNCT_2:63; :: thesis: verum