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

now

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

end;

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