const CSNo : set prop const SNo : set prop const CSNo_Re : set set axiom CSNo_ReR: !x:set.CSNo x -> SNo (CSNo_Re x) const CSNo_Im : set set axiom CSNo_ImR: !x:set.CSNo x -> SNo (CSNo_Im x) const mul_SNo : set set set term * = mul_SNo infix * 2291 2290 axiom SNo_mul_SNo: !x:set.!y:set.SNo x -> SNo y -> SNo (x * y) const add_SNo : set set set term + = add_SNo infix + 2281 2280 axiom SNo_add_SNo: !x:set.!y:set.SNo x -> SNo y -> SNo (x + y) claim !x:set.!y:set.CSNo x -> CSNo y -> SNo (CSNo_Re x * CSNo_Im y + CSNo_Im x * CSNo_Re y)