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

now :: thesis: for n being Element of NAT holds ((abs seq) * Ns) . n = (abs (seq * Ns)) . n

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
.= |.(seq . (Ns . n)).| by SEQ_1:12
.= |.((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