let S be 1-sorted ; :: thesis: ( S is real-functions-membered implies S is complex-functions-membered )
assume A1: the carrier of S is real-functions-membered ; :: according to TOPREALC:def 2 :: thesis: S is complex-functions-membered
let x be set ; :: according to VALUED_2:def 2,TOPREALC:def 1 :: thesis: ( not x in the carrier of S or x is set )
thus ( not x in the carrier of S or x is set ) by A1; :: thesis: verum