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

now

let 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:21
.= (seq " ) . (Ns . n) by VALUED_1:10
.= ((seq " ) * Ns) . n by FUNCT_2:21 ; :: thesis: verum

end;

hence (seq * Ns) " = (seq " ) * Ns by FUNCT_2:113; :: thesis: verum