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 In : set set prop term iIn = In infix iIn 2000 2000 const real : set axiom real_mul_SNo: !x:set.x iIn real -> !y:set.y iIn real -> x * y iIn real axiom real_minus_SNo: !x:set.x iIn real -> - x iIn real axiom real_add_SNo: !x:set.x iIn real -> !y:set.y iIn real -> x + y iIn real const complex : set axiom complex_I: !x:set.x iIn real -> !y:set.y iIn real -> SNo_pair x y iIn complex var x:set var y:set hyp y iIn complex hyp CSNo_Re x iIn real hyp CSNo_Im x iIn real hyp CSNo_Re y iIn real claim CSNo_Im y iIn real -> 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) iIn complex