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

now

let n be Element of NAT ; :: thesis: ((s *' ) " ) . n = ((s " ) *' ) . n
thus ((s *' ) " ) . n = ((s *' ) . n) " by VALUED_1:10
.= ((s . n) *' ) " by Def2
.= ((s . n) " ) *' by COMPLEX1:122
.= ((s " ) . n) *' by VALUED_1:10
.= ((s " ) *' ) . n by Def2 ; :: thesis: verum

end;

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