let r be Element of COMPLEX ; :: thesis: for s being Complex_Sequence holds (r (#) s) *' = (r *' ) (#) (s *' )
let s be Complex_Sequence; :: thesis: (r (#) s) *' = (r *' ) (#) (s *' )

now

let n be Element of NAT ; :: thesis: ((r (#) s) *' ) . n = ((r *' ) (#) (s *' )) . n
thus ((r (#) s) *' ) . n = ((r (#) s) . n) *' by Def2
.= (r * (s . n)) *' by VALUED_1:6
.= (r *' ) * ((s . n) *' ) by COMPLEX1:121
.= (r *' ) * ((s *' ) . n) by Def2
.= ((r *' ) (#) (s *' )) . n by VALUED_1:6 ; :: thesis: verum

end;

hence (r (#) s) *' = (r *' ) (#) (s *' ) by FUNCT_2:113; :: thesis: verum