theorem RSC: :: RVSUM_4:16

for x being object holds
( x is real-valued Complex_Sequence iff x is Real_Sequence )