theorem XCF: :: RVSUM_4:50

for c being Complex holds XFS2FS <%c%> = <*c*>