let s, s9 be Complex_Sequence; :: thesis: (s (#) s9) *' = (s *') (#) (s9 *')

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

let n be Element of NAT ; :: thesis: ((s (#) s9) *') . n = ((s *') (#) (s9 *')) . n
thus ((s (#) s9) *') . n = ((s (#) s9) . n) *' by Def2
.= ((s . n) * (s9 . n)) *' by VALUED_1:5
.= ((s . n) *') * ((s9 . n) *') by COMPLEX1:35
.= ((s *') . n) * ((s9 . n) *') by Def2
.= ((s *') . n) * ((s9 *') . n) by Def2
.= ((s *') (#) (s9 *')) . n by VALUED_1:5 ; :: thesis: verum

end;

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