const SNo : set prop 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 CSNo : set prop const add_SNo : set set set term + = add_SNo infix + 2281 2280 const CSNo_Re : set set const CSNo_Im : set set const ordsucc : set set const Empty : set const mul_CSNo : set set set const Complex_i : set const minus_CSNo : set set const add_CSNo : set set set lemma !x:set.!y:set.CSNo x -> SNo y -> (CSNo_Re x * CSNo_Re x + CSNo_Im x * CSNo_Im x) * y = ordsucc Empty -> SNo (CSNo_Re x) -> SNo (CSNo_Im x) -> SNo (y * CSNo_Re x) -> CSNo (y * CSNo_Re x) -> SNo (y * CSNo_Im x) -> CSNo (y * CSNo_Im x) -> CSNo (mul_CSNo Complex_i (y * CSNo_Im x)) -> CSNo (minus_CSNo (mul_CSNo Complex_i (y * CSNo_Im x))) -> CSNo (add_CSNo (y * CSNo_Re x) (minus_CSNo (mul_CSNo Complex_i (y * CSNo_Im x)))) -> SNo (CSNo_Re x * CSNo_Re x) -> mul_CSNo x (add_CSNo (y * CSNo_Re x) (minus_CSNo (mul_CSNo Complex_i (y * CSNo_Im x)))) = ordsucc Empty var x:set var y:set hyp CSNo x hyp SNo y hyp (CSNo_Re x * CSNo_Re x + CSNo_Im x * CSNo_Im x) * y = ordsucc Empty hyp SNo (CSNo_Re x) hyp SNo (CSNo_Im x) hyp SNo (y * CSNo_Re x) hyp CSNo (y * CSNo_Re x) hyp SNo (y * CSNo_Im x) hyp CSNo (y * CSNo_Im x) hyp CSNo (mul_CSNo Complex_i (y * CSNo_Im x)) hyp CSNo (minus_CSNo (mul_CSNo Complex_i (y * CSNo_Im x))) claim CSNo (add_CSNo (y * CSNo_Re x) (minus_CSNo (mul_CSNo Complex_i (y * CSNo_Im x)))) -> mul_CSNo x (add_CSNo (y * CSNo_Re x) (minus_CSNo (mul_CSNo Complex_i (y * CSNo_Im x)))) = ordsucc Empty