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

now :: thesis: for n being Element of NAT holds ((r (#) s) *') . n = ((r *') (#) (s *')) . n

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:35
.= (r *') * ((s *') . n) by Def2
.= ((r *') (#) (s *')) . n by VALUED_1:6 ; :: thesis: verum

end;

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