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

let Ns be V43() sequence of NAT; :: thesis: (seq * Ns) " = (seq ") * Ns

let Ns be V43() sequence of NAT; :: thesis: (seq * Ns) " = (seq ") * Ns

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

hence
(seq * Ns) " = (seq ") * Ns
by FUNCT_2:63; :: thesis: verumlet n be Element of NAT ; :: thesis: ((seq * Ns) ") . n = ((seq ") * Ns) . n

thus ((seq * Ns) ") . n = ((seq * Ns) . n) " by VALUED_1:10

.= (seq . (Ns . n)) " by FUNCT_2:15

.= (seq ") . (Ns . n) by VALUED_1:10

.= ((seq ") * Ns) . n by FUNCT_2:15 ; :: thesis: verum

end;thus ((seq * Ns) ") . n = ((seq * Ns) . n) " by VALUED_1:10

.= (seq . (Ns . n)) " by FUNCT_2:15

.= (seq ") . (Ns . n) by VALUED_1:10

.= ((seq ") * Ns) . n by FUNCT_2:15 ; :: thesis: verum