let s be Complex_Sequence; :: thesis: (s *') " = (s ") *'
now :: thesis: for n being Element of NAT holds ((s *') ") . n = ((s ") *') . n
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:36
.= ((s ") . n) *' by VALUED_1:10
.= ((s ") *') . n by Def2 ; :: thesis: verum
end;
hence (s *') " = (s ") *' by FUNCT_2:63; :: thesis: verum