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

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

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:35
.= ((s9 . n) *') * (((s . n) *') ") by COMPLEX1:36
.= ((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:63; :: thesis: verum