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

now

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:121
.= ((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:113; :: thesis: verum