const SNo_pair : set set set const add_SNo : set set set term + = add_SNo infix + 2281 2280 const mul_SNo : set set set term * = mul_SNo infix * 2291 2290 const CSNo_Re : set set const minus_SNo : set set term - = minus_SNo const CSNo_Im : set set term mul_CSNo = \x:set.\y:set.SNo_pair (CSNo_Re x * CSNo_Re y + - CSNo_Im x * CSNo_Im y) (CSNo_Re x * CSNo_Im y + CSNo_Im x * CSNo_Re y) const CSNo : set prop const SNo : set prop axiom mul_CSNo_ReR: !x:set.!y:set.CSNo x -> CSNo y -> SNo (CSNo_Re x * CSNo_Re y + - CSNo_Im x * CSNo_Im y) axiom mul_CSNo_ImR: !x:set.!y:set.CSNo x -> CSNo y -> SNo (CSNo_Re x * CSNo_Im y + CSNo_Im x * CSNo_Re y) axiom CSNo_Re2: !x:set.!y:set.SNo x -> SNo y -> CSNo_Re (SNo_pair x y) = x claim !x:set.!y:set.CSNo x -> CSNo y -> CSNo_Re (mul_CSNo x y) = CSNo_Re x * CSNo_Re y + - CSNo_Im x * CSNo_Im y