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

now

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

end;

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