let seq be Real_Sequence; :: thesis: for Ns being V43() sequence of NAT holds

( (- seq) * Ns = - (seq * Ns) & (abs seq) * Ns = abs (seq * Ns) )

let Ns be V43() 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)

( (- seq) * Ns = - (seq * Ns) & (abs seq) * Ns = abs (seq * Ns) )

let Ns be V43() 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

hence
(abs seq) * Ns = abs (seq * Ns)
by FUNCT_2:63; :: thesis: verumlet 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;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