include('Axioms/HolSmt^2.ax').
thf(tp_c_2Ecomplex_2EIM,type,(c_2Ecomplex_2EIM:$i)).
thf(mem_c_2Ecomplex_2EIM,axiom,(mem@c_2Ecomplex_2EIM@(arr@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@ty_2Erealax_2Ereal))).
thf(stp_fo_c_2Ecomplex_2EIM,type,(fo__c_2Ecomplex_2EIM:(tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal > tp__ty_2Erealax_2Ereal))).
thf(stp_eq_fo_c_2Ecomplex_2EIM,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((inj__ty_2Erealax_2Ereal @ (fo__c_2Ecomplex_2EIM @ X0)) = (ap @ c_2Ecomplex_2EIM @ (inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ X0))))).
thf(tp_c_2Ecomplex_2ERE,type,(c_2Ecomplex_2ERE:$i)).
thf(mem_c_2Ecomplex_2ERE,axiom,(mem@c_2Ecomplex_2ERE@(arr@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@ty_2Erealax_2Ereal))).
thf(stp_fo_c_2Ecomplex_2ERE,type,(fo__c_2Ecomplex_2ERE:(tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal > tp__ty_2Erealax_2Ereal))).
thf(stp_eq_fo_c_2Ecomplex_2ERE,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((inj__ty_2Erealax_2Ereal @ (fo__c_2Ecomplex_2ERE @ X0)) = (ap @ c_2Ecomplex_2ERE @ (inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ X0))))).
thf(tp_c_2Ecomplex_2Earg,type,(c_2Ecomplex_2Earg:$i)).
thf(mem_c_2Ecomplex_2Earg,axiom,(mem@c_2Ecomplex_2Earg@(arr@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@ty_2Erealax_2Ereal))).
thf(stp_fo_c_2Ecomplex_2Earg,type,(fo__c_2Ecomplex_2Earg:(tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal > tp__ty_2Erealax_2Ereal))).
thf(stp_eq_fo_c_2Ecomplex_2Earg,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((inj__ty_2Erealax_2Ereal @ (fo__c_2Ecomplex_2Earg @ X0)) = (ap @ c_2Ecomplex_2Earg @ (inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ X0))))).
thf(tp_c_2Ecomplex_2Ecomplex__add,type,(c_2Ecomplex_2Ecomplex__add:$i)).
thf(mem_c_2Ecomplex_2Ecomplex__add,axiom,(mem@c_2Ecomplex_2Ecomplex__add@(arr@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(arr@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal))))).
thf(tp_c_2Ecomplex_2Ecomplex__div,type,(c_2Ecomplex_2Ecomplex__div:$i)).
thf(mem_c_2Ecomplex_2Ecomplex__div,axiom,(mem@c_2Ecomplex_2Ecomplex__div@(arr@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(arr@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal))))).
thf(tp_c_2Ecomplex_2Ecomplex__exp,type,(c_2Ecomplex_2Ecomplex__exp:$i)).
thf(mem_c_2Ecomplex_2Ecomplex__exp,axiom,(mem@c_2Ecomplex_2Ecomplex__exp@(arr@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)))).
thf(tp_c_2Ecomplex_2Ecomplex__inv,type,(c_2Ecomplex_2Ecomplex__inv:$i)).
thf(mem_c_2Ecomplex_2Ecomplex__inv,axiom,(mem@c_2Ecomplex_2Ecomplex__inv@(arr@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)))).
thf(tp_c_2Ecomplex_2Ecomplex__mul,type,(c_2Ecomplex_2Ecomplex__mul:$i)).
thf(mem_c_2Ecomplex_2Ecomplex__mul,axiom,(mem@c_2Ecomplex_2Ecomplex__mul@(arr@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(arr@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal))))).
thf(tp_c_2Ecomplex_2Ecomplex__neg,type,(c_2Ecomplex_2Ecomplex__neg:$i)).
thf(mem_c_2Ecomplex_2Ecomplex__neg,axiom,(mem@c_2Ecomplex_2Ecomplex__neg@(arr@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)))).
thf(tp_c_2Ecomplex_2Ecomplex__of__num,type,(c_2Ecomplex_2Ecomplex__of__num:$i)).
thf(mem_c_2Ecomplex_2Ecomplex__of__num,axiom,(mem@c_2Ecomplex_2Ecomplex__of__num@(arr@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)))).
thf(tp_c_2Ecomplex_2Ecomplex__of__real,type,(c_2Ecomplex_2Ecomplex__of__real:$i)).
thf(mem_c_2Ecomplex_2Ecomplex__of__real,axiom,(mem@c_2Ecomplex_2Ecomplex__of__real@(arr@ty_2Erealax_2Ereal@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)))).
thf(tp_c_2Ecomplex_2Ecomplex__pow,type,(c_2Ecomplex_2Ecomplex__pow:$i)).
thf(mem_c_2Ecomplex_2Ecomplex__pow,axiom,(mem@c_2Ecomplex_2Ecomplex__pow@(arr@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(arr@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal))))).
thf(tp_c_2Ecomplex_2Ecomplex__scalar__lmul,type,(c_2Ecomplex_2Ecomplex__scalar__lmul:$i)).
thf(mem_c_2Ecomplex_2Ecomplex__scalar__lmul,axiom,(mem@c_2Ecomplex_2Ecomplex__scalar__lmul@(arr@ty_2Erealax_2Ereal@(arr@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal))))).
thf(tp_c_2Ecomplex_2Ecomplex__scalar__rmul,type,(c_2Ecomplex_2Ecomplex__scalar__rmul:$i)).
thf(mem_c_2Ecomplex_2Ecomplex__scalar__rmul,axiom,(mem@c_2Ecomplex_2Ecomplex__scalar__rmul@(arr@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(arr@ty_2Erealax_2Ereal@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal))))).
thf(tp_c_2Ecomplex_2Ecomplex__sub,type,(c_2Ecomplex_2Ecomplex__sub:$i)).
thf(mem_c_2Ecomplex_2Ecomplex__sub,axiom,(mem@c_2Ecomplex_2Ecomplex__sub@(arr@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(arr@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal))))).
thf(tp_c_2Ecomplex_2Econj,type,(c_2Ecomplex_2Econj:$i)).
thf(mem_c_2Ecomplex_2Econj,axiom,(mem@c_2Ecomplex_2Econj@(arr@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)))).
thf(tp_c_2Ecomplex_2Ei,type,(c_2Ecomplex_2Ei:$i)).
thf(mem_c_2Ecomplex_2Ei,axiom,(mem@c_2Ecomplex_2Ei@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal))).
thf(tp_c_2Ecomplex_2Emodu,type,(c_2Ecomplex_2Emodu:$i)).
thf(mem_c_2Ecomplex_2Emodu,axiom,(mem@c_2Ecomplex_2Emodu@(arr@(ty_2Epair_2Eprod@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@ty_2Erealax_2Ereal))).
thf(stp_fo_c_2Ecomplex_2Emodu,type,(fo__c_2Ecomplex_2Emodu:(tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal > tp__ty_2Erealax_2Ereal))).
thf(stp_eq_fo_c_2Ecomplex_2Emodu,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((inj__ty_2Erealax_2Ereal @ (fo__c_2Ecomplex_2Emodu @ X0)) = (ap @ c_2Ecomplex_2Emodu @ (inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ X0))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__LEMMA1,lemma,( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1b:tp__ty_2Erealax_2Ereal] : ( ! [V2c:tp__ty_2Erealax_2Ereal] : ( ! [V3d:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Erealax_2Ereal__add@(ap@(ap@c_2Ereal_2Epow@(ap@(ap@c_2Ereal_2Ereal__sub@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V0a))@(inj__ty_2Erealax_2Ereal @ V2c)))@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V1b))@(inj__ty_2Erealax_2Ereal @ V3d))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(ap@c_2Ereal_2Epow@(ap@(ap@c_2Erealax_2Ereal__add@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V0a))@(inj__ty_2Erealax_2Ereal @ V3d)))@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V1b))@(inj__ty_2Erealax_2Ereal @ V2c))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Erealax_2Ereal__mul@(ap@(ap@c_2Erealax_2Ereal__add@(ap@(ap@c_2Ereal_2Epow@(inj__ty_2Erealax_2Ereal @ V0a))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(ap@c_2Ereal_2Epow@(inj__ty_2Erealax_2Ereal @ V1b))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(ap@(ap@c_2Erealax_2Ereal__add@(ap@(ap@c_2Ereal_2Epow@(inj__ty_2Erealax_2Ereal @ V2c))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(ap@c_2Ereal_2Epow@(inj__ty_2Erealax_2Ereal @ V3d))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__LEMMA2,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Eabs@(inj__ty_2Erealax_2Ereal @ V0x)))@(ap@c_2Etransc_2Esqrt@(ap@(ap@c_2Erealax_2Ereal__add@(ap@(ap@c_2Ereal_2Epow@(inj__ty_2Erealax_2Ereal @ V0x))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(ap@c_2Ereal_2Epow@(inj__ty_2Erealax_2Ereal @ V1y))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))).
thf(ax_thm_2Ecomplex_2ERE,axiom,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2ERE@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__ty_2Erealax_2Ereal @ (ap@(c_2Epair_2EFST@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))))).
thf(ax_thm_2Ecomplex_2EIM,axiom,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2EIM@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__ty_2Erealax_2Ereal @ (ap@(c_2Epair_2ESND@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(ap@c_2Ecomplex_2ERE@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Ecomplex_2EIM@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))) = V0z))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__RE__IM__EQ,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((V0z = V1w) <=> (((surj__ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2ERE@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2ERE@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))) & ((surj__ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2EIM@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2EIM@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))))))))).
thf(ax_thm_2Ecomplex_2Ecomplex__of__real,axiom,( ! [V0x:tp__ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__real@(inj__ty_2Erealax_2Ereal @ V0x))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(inj__ty_2Erealax_2Ereal @ V0x))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))).
thf(conj_thm_2Ecomplex_2ERE__COMPLEX__OF__REAL,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2ERE@(ap@c_2Ecomplex_2Ecomplex__of__real@(inj__ty_2Erealax_2Ereal @ V0x)))) = V0x))).
thf(conj_thm_2Ecomplex_2EIM__COMPLEX__OF__REAL,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2EIM@(ap@c_2Ecomplex_2Ecomplex__of__real@(inj__ty_2Erealax_2Ereal @ V0x)))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))).
thf(ax_thm_2Ecomplex_2Ecomplex__of__num,axiom,( ! [V0n:tp__ty_2Enum_2Enum] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ V0n))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__real@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ V0n))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__0,lemma,((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__real@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__1,lemma,((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__real@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__10,lemma,(~~ ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__0__THM,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) <=> ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Erealax_2Ereal__add@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ecomplex_2ERE@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ecomplex_2EIM@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))).
thf(ax_thm_2Ecomplex_2Ei,axiom,((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ c_2Ecomplex_2Ei) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))).
thf(ax_thm_2Ecomplex_2Ecomplex__add,axiom,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(ap@(ap@c_2Erealax_2Ereal__add@(ap@c_2Ecomplex_2ERE@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Ecomplex_2ERE@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))))@(ap@(ap@c_2Erealax_2Ereal__add@(ap@c_2Ecomplex_2EIM@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Ecomplex_2EIM@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))))))))).
thf(ax_thm_2Ecomplex_2Ecomplex__neg,axiom,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(ap@c_2Erealax_2Ereal__neg@(ap@c_2Ecomplex_2ERE@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))))@(ap@c_2Erealax_2Ereal__neg@(ap@c_2Ecomplex_2EIM@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))))))).
thf(ax_thm_2Ecomplex_2Ecomplex__mul,axiom,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(ap@(ap@c_2Ereal_2Ereal__sub@(ap@(ap@c_2Erealax_2Ereal__mul@(ap@c_2Ecomplex_2ERE@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Ecomplex_2ERE@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))))@(ap@(ap@c_2Erealax_2Ereal__mul@(ap@c_2Ecomplex_2EIM@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Ecomplex_2EIM@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))))@(ap@(ap@c_2Erealax_2Ereal__add@(ap@(ap@c_2Erealax_2Ereal__mul@(ap@c_2Ecomplex_2ERE@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Ecomplex_2EIM@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))))@(ap@(ap@c_2Erealax_2Ereal__mul@(ap@c_2Ecomplex_2EIM@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Ecomplex_2ERE@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))))))))).
thf(ax_thm_2Ecomplex_2Ecomplex__inv,axiom,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__inv@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(ap@(ap@c_2Ereal_2E_2F@(ap@c_2Ecomplex_2ERE@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@(ap@c_2Erealax_2Ereal__add@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ecomplex_2ERE@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ecomplex_2EIM@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(ap@(ap@c_2Ereal_2E_2F@(ap@c_2Erealax_2Ereal__neg@(ap@c_2Ecomplex_2EIM@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))))@(ap@(ap@c_2Erealax_2Ereal__add@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ecomplex_2ERE@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ecomplex_2EIM@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))).
thf(ax_thm_2Ecomplex_2Ecomplex__sub,axiom,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))))))).
thf(ax_thm_2Ecomplex_2Ecomplex__div,axiom,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(ap@c_2Ecomplex_2Ecomplex__inv@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__ADD__COMM,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__ADD__ASSOC,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__ADD__RID,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) = V0z))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__ADD__LID,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = V0z))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__ADD__RINV,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__ADD__LINV,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__MUL__COMM,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__MUL__ASSOC,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__MUL__RID,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(ap@c_2Ecomplex_2Ecomplex__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) = V0z))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__MUL__LID,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(ap@c_2Ecomplex_2Ecomplex__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = V0z))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__MUL__RINV,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((~~ (V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) => ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(ap@c_2Ecomplex_2Ecomplex__inv@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__MUL__LINV,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((~~ (V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) => ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(ap@c_2Ecomplex_2Ecomplex__inv@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__ADD__LDISTRIB,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__ADD__RDISTRIB,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v)))@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__EQ__LADD,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v)))) <=> (V1w = V2v)))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__EQ__RADD,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v)))) <=> (V0z = V1w)))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__ADD__RID__UNIQ,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))) = V0z) <=> (V1w = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__ADD__LID__UNIQ,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))) = V1w) <=> (V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__NEGNEG,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))) = V0z))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__NEG__EQ,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = V1w) <=> (V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__EQ__NEG,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))) <=> (V0z = V1w))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__RNEG__UNIQ,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) <=> (V1w = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__LNEG__UNIQ,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) <=> (V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__NEG__ADD,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__MUL__RZERO,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__MUL__LZERO,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__NEG__LMUL,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__NEG__RMUL,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__NEG__MUL2,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__ENTIRE,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) <=> ((V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) | (V1w = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__NEG__0,lemma,((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__NEG__EQ0,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) <=> (V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SUB__REFL,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SUB__RZERO,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) = V0z))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SUB__LZERO,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SUB__LNEG,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SUB__NEG2,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__NEG__SUB,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SUB__RNEG,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SUB__ADD,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))) = V0z)))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SUB__ADD2,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))) = V0z)))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__ADD__SUB,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = V1w)))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SUB__SUB,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SUB__SUB2,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))) = V1w)))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__ADD__SUB2,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__ADD2__SUB2,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2u:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V3v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))@(ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2u))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V3v)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2u)))@(ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V3v)))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SUB__TRIANGLE,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))@(ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SUB__0,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) <=> (V0z = V1w))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__EQ__SUB__LADD,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v)))) <=> ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v))) = V1w)))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__EQ__SUB__RADD,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))) = V2v) <=> (V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__MUL__RNEG,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__MUL__LNEG,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SUB__LDISTRIB,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SUB__RDISTRIB,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v)))@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__DIFFSQ,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))@(ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__EQ__LMUL,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v)))) <=> ((V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) | (V1w = V2v))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__EQ__RMUL,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v)))) <=> ((V2v = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) | (V0z = V1w))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__EQ__LMUL2,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((~~ (V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) => ((V1w = V2v) <=> ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v)))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__EQ__RMUL__IMP,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((~~ (V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))))) => (V1w = V2v)))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__EQ__LMUL__IMP,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((~~ (V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v))))) => (V1w = V2v)))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__NEG__INV,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((~~ (V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) => ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__inv@(ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(ap@c_2Ecomplex_2Ecomplex__inv@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__INV__MUL,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((~~ (V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & (~~ (V1w = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))) => ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__inv@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(ap@c_2Ecomplex_2Ecomplex__inv@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Ecomplex_2Ecomplex__inv@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__INVINV,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((~~ (V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) => ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__inv@(ap@c_2Ecomplex_2Ecomplex__inv@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))) = V0z)))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__LINV__UNIQ,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) => (V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__inv@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__RINV__UNIQ,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) => (V1w = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__inv@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__INV__0,lemma,((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__inv@(ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__INV1,lemma,((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__inv@(ap@c_2Ecomplex_2Ecomplex__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__INV__INV,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__inv@(ap@c_2Ecomplex_2Ecomplex__inv@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))) = V0z))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__INV__NEG,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__inv@(ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(ap@c_2Ecomplex_2Ecomplex__inv@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__INV__EQ__0,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__inv@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) <=> (V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__INV__NZ,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((~~ (V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) => (~~ ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__inv@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__INV__INJ,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__inv@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__inv@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))) <=> (V0z = V1w))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__NEG__LDIV,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__NEG__RDIV,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__NEG__DIV2,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__INV__1OVER,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__inv@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(ap@c_2Ecomplex_2Ecomplex__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__DIV1,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(ap@c_2Ecomplex_2Ecomplex__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) = V0z))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__DIV__ADD,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v)))@(ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__DIV__SUB,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v)))@(ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__DIV__RMUL__CANCEL,lemma,( ! [V0v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((~~ (V0v = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) => ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0v)))@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0v)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2w))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__DIV__LMUL__CANCEL,lemma,( ! [V0v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((~~ (V0v = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) => ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0v))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z)))@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0v))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2w)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2w))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__DIV__DENOM__CANCEL,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((~~ (V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) => ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__DIV__INNER__CANCEL,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((~~ (V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) => ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__DIV__OUTER__CANCEL,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((~~ (V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) => ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))@(ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__DIV__MUL2,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((~~ (V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & (~~ (V1w = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))) => ( ! [V2v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v)))@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__ADD__RAT,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2u:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V3v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((~~ (V1w = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & (~~ (V3v = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))) => ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))@(ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2u))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V3v)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(ap@(ap@c_2Ecomplex_2Ecomplex__add@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V3v)))@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2u))))@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V3v))))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SUB__RAT,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2u:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V3v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((~~ (V1w = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & (~~ (V3v = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))) => ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))@(ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2u))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V3v)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(ap@(ap@c_2Ecomplex_2Ecomplex__sub@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V3v)))@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2u))))@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V3v))))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__DIV__LZERO,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__DIV__REFL,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((~~ (V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) => ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SUB__INV2,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((~~ (V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & (~~ (V1w = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))) => ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(ap@c_2Ecomplex_2Ecomplex__inv@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Ecomplex_2Ecomplex__inv@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__EQ__RDIV__EQ,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((~~ (V2v = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) => ((V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v)))) <=> ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v))) = V1w))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__EQ__LDIV__EQ,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2v:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((~~ (V2v = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) => (((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v))) = V1w) <=> (V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2v)))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__OF__REAL__EQ,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : (((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__real@(inj__ty_2Erealax_2Ereal @ V0x))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__real@(inj__ty_2Erealax_2Ereal @ V1y)))) <=> (V0x = V1y))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__OF__REAL__ADD,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(ap@c_2Ecomplex_2Ecomplex__of__real@(inj__ty_2Erealax_2Ereal @ V0x)))@(ap@c_2Ecomplex_2Ecomplex__of__real@(inj__ty_2Erealax_2Ereal @ V1y)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__real@(ap@(ap@c_2Erealax_2Ereal__add@(inj__ty_2Erealax_2Ereal @ V0x))@(inj__ty_2Erealax_2Ereal @ V1y)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__OF__REAL__NEG,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(ap@c_2Ecomplex_2Ecomplex__of__real@(inj__ty_2Erealax_2Ereal @ V0x)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__real@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V0x))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__OF__REAL__MUL,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(ap@c_2Ecomplex_2Ecomplex__of__real@(inj__ty_2Erealax_2Ereal @ V0x)))@(ap@c_2Ecomplex_2Ecomplex__of__real@(inj__ty_2Erealax_2Ereal @ V1y)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__real@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V0x))@(inj__ty_2Erealax_2Ereal @ V1y)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__OF__REAL__INV,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__inv@(ap@c_2Ecomplex_2Ecomplex__of__real@(inj__ty_2Erealax_2Ereal @ V0x)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__real@(ap@c_2Erealax_2Einv@(inj__ty_2Erealax_2Ereal @ V0x))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__OF__REAL__SUB,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(ap@c_2Ecomplex_2Ecomplex__of__real@(inj__ty_2Erealax_2Ereal @ V0x)))@(ap@c_2Ecomplex_2Ecomplex__of__real@(inj__ty_2Erealax_2Ereal @ V1y)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__real@(ap@(ap@c_2Ereal_2Ereal__sub@(inj__ty_2Erealax_2Ereal @ V0x))@(inj__ty_2Erealax_2Ereal @ V1y)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__OF__REAL__DIV,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(ap@c_2Ecomplex_2Ecomplex__of__real@(inj__ty_2Erealax_2Ereal @ V0x)))@(ap@c_2Ecomplex_2Ecomplex__of__real@(inj__ty_2Erealax_2Ereal @ V1y)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__real@(ap@(ap@c_2Ereal_2E_2F@(inj__ty_2Erealax_2Ereal @ V0x))@(inj__ty_2Erealax_2Ereal @ V1y)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__OF__NUM__EQ,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ V0m))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ V1n)))) <=> (V0m = V1n))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__OF__NUM__ADD,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ V0m)))@(ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ V1n)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__OF__NUM__MUL,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ V0m)))@(ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ V1n)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n)))))))).
thf(ax_thm_2Ecomplex_2Ecomplex__scalar__lmul,axiom,( ! [V0k:tp__ty_2Erealax_2Ereal] : ( ! [V1z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V0k))@(ap@c_2Ecomplex_2ERE@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z))))@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V0k))@(ap@c_2Ecomplex_2EIM@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z))))))))).
thf(ax_thm_2Ecomplex_2Ecomplex__scalar__rmul,axiom,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1k:tp__ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__rmul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__ty_2Erealax_2Ereal @ V1k))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(ap@(ap@c_2Erealax_2Ereal__mul@(ap@c_2Ecomplex_2ERE@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(inj__ty_2Erealax_2Ereal @ V1k)))@(ap@(ap@c_2Erealax_2Ereal__mul@(ap@c_2Ecomplex_2EIM@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(inj__ty_2Erealax_2Ereal @ V1k)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__LMUL,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : ( ! [V1l:tp__ty_2Erealax_2Ereal] : ( ! [V2z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V1l))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2z)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__ty_2Erealax_2Ereal @ V1l)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2z)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__LMUL__NEG,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : ( ! [V1z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V0k)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__NEG__SCALAR__LMUL,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : ( ! [V1z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V0k)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__LMUL__ADD,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : ( ! [V1l:tp__ty_2Erealax_2Ereal] : ( ! [V2z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(ap@(ap@c_2Erealax_2Ereal__add@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__ty_2Erealax_2Ereal @ V1l)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2z)))@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V1l))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2z))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__LMUL__SUB,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : ( ! [V1l:tp__ty_2Erealax_2Ereal] : ( ! [V2z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(ap@(ap@c_2Ereal_2Ereal__sub@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__ty_2Erealax_2Ereal @ V1l)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2z)))@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V1l))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2z))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__ADD__SCALAR__LMUL,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : ( ! [V1z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2w)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z)))@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2w))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SUB__SCALAR__LMUL,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : ( ! [V1z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2w)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z)))@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2w))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__MUL__SCALAR__LMUL2,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : ( ! [V1l:tp__ty_2Erealax_2Ereal] : ( ! [V2z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V3w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2z)))@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V1l))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V3w)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__ty_2Erealax_2Ereal @ V1l)))@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V3w)))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__LMUL__SCALAR__LMUL,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : ( ! [V1z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2w))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2w))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__RMUL__SCALAR__LMUL,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : ( ! [V1z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z))@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2w)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2w))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__LMUL__ZERO,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__ZERO__SCALAR__LMUL,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__LMUL__ONE,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = V0z))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__LMUL__NEG1,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(ap@c_2Erealax_2Ereal__neg@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__DOUBLE,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__LMUL__ENTIRE,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : ( ! [V1z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) <=> ((V0k = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) | (V1z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__EQ__SCALAR__LMUL,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : ( ! [V1z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2w)))) <=> ((V0k = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) | (V1z = V2w))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__LMUL__EQ,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : ( ! [V1l:tp__ty_2Erealax_2Ereal] : ( ! [V2z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V1l))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2z)))) <=> ((V0k = V1l) | (V2z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__LMUL__EQ1,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : ( ! [V1z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z))) = V1z) <=> ((V0k = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) | (V1z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__INV__SCALAR__LMUL,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : ( ! [V1z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((~~ (V0k = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & (~~ (V1z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))) => ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__inv@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(ap@c_2Erealax_2Einv@(inj__ty_2Erealax_2Ereal @ V0k)))@(ap@c_2Ecomplex_2Ecomplex__inv@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__LMUL__DIV2,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : ( ! [V1l:tp__ty_2Erealax_2Ereal] : ( ! [V2z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V3w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((~~ (V1l = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & (~~ (V3w = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))) => ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2z)))@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V1l))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V3w)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(ap@(ap@c_2Ereal_2E_2F@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__ty_2Erealax_2Ereal @ V1l)))@(ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V3w))))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__MUL__COMM,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : ( ! [V1z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__rmul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z))@(inj__ty_2Erealax_2Ereal @ V0k))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__RMUL,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : ( ! [V1l:tp__ty_2Erealax_2Ereal] : ( ! [V2z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__rmul@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__rmul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2z))@(inj__ty_2Erealax_2Ereal @ V0k)))@(inj__ty_2Erealax_2Ereal @ V1l))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__rmul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2z))@(ap@(ap@c_2Erealax_2Ereal__mul@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__ty_2Erealax_2Ereal @ V1l))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__RMUL__NEG,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : ( ! [V1z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__rmul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z))@(inj__ty_2Erealax_2Ereal @ V0k)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__rmul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z))@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V0k)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__NEG__SCALAR__RMUL,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : ( ! [V1z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__rmul@(ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z)))@(inj__ty_2Erealax_2Ereal @ V0k))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__rmul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z))@(ap@c_2Erealax_2Ereal__neg@(inj__ty_2Erealax_2Ereal @ V0k)))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__RMUL__ADD,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : ( ! [V1l:tp__ty_2Erealax_2Ereal] : ( ! [V2z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__rmul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2z))@(ap@(ap@c_2Erealax_2Ereal__add@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__ty_2Erealax_2Ereal @ V1l)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__rmul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2z))@(inj__ty_2Erealax_2Ereal @ V0k)))@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__rmul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2z))@(inj__ty_2Erealax_2Ereal @ V1l))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__RSCALAR__RMUL__SUB,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : ( ! [V1l:tp__ty_2Erealax_2Ereal] : ( ! [V2z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__rmul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2z))@(ap@(ap@c_2Ereal_2Ereal__sub@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__ty_2Erealax_2Ereal @ V1l)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__rmul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2z))@(inj__ty_2Erealax_2Ereal @ V0k)))@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__rmul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2z))@(inj__ty_2Erealax_2Ereal @ V1l))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__ADD__RSCALAR__RMUL,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : ( ! [V1z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__rmul@(ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2w)))@(inj__ty_2Erealax_2Ereal @ V0k))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__rmul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z))@(inj__ty_2Erealax_2Ereal @ V0k)))@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__rmul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2w))@(inj__ty_2Erealax_2Ereal @ V0k))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SUB__SCALAR__RMUL,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : ( ! [V1z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V2w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__rmul@(ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2w)))@(inj__ty_2Erealax_2Ereal @ V0k))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__rmul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z))@(inj__ty_2Erealax_2Ereal @ V0k)))@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__rmul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V2w))@(inj__ty_2Erealax_2Ereal @ V0k))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__RMUL__ZERO,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__rmul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__ZERO__SCALAR__RMUL,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__rmul@(ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(inj__ty_2Erealax_2Ereal @ V0k))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__RMUL__ONE,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__rmul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) = V0z))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__SCALAR__RMUL__NEG1,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__rmul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(ap@c_2Erealax_2Ereal__neg@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))))).
thf(ax_thm_2Ecomplex_2Econj,axiom,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Econj@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@(c_2Epair_2E_2C@ty_2Erealax_2Ereal@ty_2Erealax_2Ereal)@(ap@c_2Ecomplex_2ERE@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Erealax_2Ereal__neg@(ap@c_2Ecomplex_2EIM@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))))))).
thf(conj_thm_2Ecomplex_2ECONJ__REAL__REFL,lemma,( ! [V0x:tp__ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Econj@(ap@c_2Ecomplex_2Ecomplex__of__real@(inj__ty_2Erealax_2Ereal @ V0x)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__real@(inj__ty_2Erealax_2Ereal @ V0x)))))).
thf(conj_thm_2Ecomplex_2ECONJ__NUM__REFL,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Econj@(ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ V0n)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ V0n)))))).
thf(conj_thm_2Ecomplex_2ECONJ__ADD,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Econj@(ap@(ap@c_2Ecomplex_2Ecomplex__add@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__add@(ap@c_2Ecomplex_2Econj@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Ecomplex_2Econj@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))))))).
thf(conj_thm_2Ecomplex_2ECONJ__NEG,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Econj@(ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__neg@(ap@c_2Ecomplex_2Econj@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))))))).
thf(conj_thm_2Ecomplex_2ECONJ__SUB,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Econj@(ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__sub@(ap@c_2Ecomplex_2Econj@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Ecomplex_2Econj@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))))))).
thf(conj_thm_2Ecomplex_2ECONJ__MUL,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Econj@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(ap@c_2Ecomplex_2Econj@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Ecomplex_2Econj@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))))))).
thf(conj_thm_2Ecomplex_2ECONJ__INV,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Econj@(ap@c_2Ecomplex_2Ecomplex__inv@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__inv@(ap@c_2Ecomplex_2Econj@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))))))).
thf(conj_thm_2Ecomplex_2ECONJ__DIV,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Econj@(ap@(ap@c_2Ecomplex_2Ecomplex__div@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__div@(ap@c_2Ecomplex_2Econj@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Ecomplex_2Econj@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))))))).
thf(conj_thm_2Ecomplex_2ECONJ__SCALAR__LMUL,lemma,( ! [V0k:tp__ty_2Erealax_2Ereal] : ( ! [V1z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Econj@(ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__scalar__lmul@(inj__ty_2Erealax_2Ereal @ V0k))@(ap@c_2Ecomplex_2Econj@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1z)))))))).
thf(conj_thm_2Ecomplex_2ECONJ__CONJ,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Econj@(ap@c_2Ecomplex_2Econj@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))) = V0z))).
thf(conj_thm_2Ecomplex_2ECONJ__EQ,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Econj@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = V1w) <=> (V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Econj@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))))))).
thf(conj_thm_2Ecomplex_2ECONJ__EQ2,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Econj@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Econj@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))) <=> (V0z = V1w))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__MUL__RCONJ,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(ap@c_2Ecomplex_2Econj@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__real@(ap@(ap@c_2Erealax_2Ereal__add@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ecomplex_2ERE@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ecomplex_2EIM@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__MUL__LCONJ,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(ap@c_2Ecomplex_2Econj@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__real@(ap@(ap@c_2Erealax_2Ereal__add@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ecomplex_2ERE@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ecomplex_2EIM@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))).
thf(conj_thm_2Ecomplex_2ECONJ__ZERO,lemma,((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Econj@(ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))).
thf(ax_thm_2Ecomplex_2Emodu,axiom,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Emodu@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Etransc_2Esqrt@(ap@(ap@c_2Erealax_2Ereal__add@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ecomplex_2ERE@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ecomplex_2EIM@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))).
thf(ax_thm_2Ecomplex_2Earg,axiom,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Earg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Erealax_2Ereal)@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@c_2Ecomplex_2EIM@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))))@(ap@c_2Etransc_2Eacs@(ap@(ap@c_2Ereal_2E_2F@(ap@c_2Ecomplex_2ERE@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Ecomplex_2Emodu@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))))@(ap@(ap@c_2Erealax_2Ereal__add@(ap@c_2Erealax_2Ereal__neg@(ap@c_2Etransc_2Eacs@(ap@(ap@c_2Ereal_2E_2F@(ap@c_2Ecomplex_2ERE@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Ecomplex_2Emodu@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))))))@(ap@(ap@c_2Erealax_2Ereal__mul@(ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(inj__ty_2Erealax_2Ereal @ fo__c_2Etransc_2Epi)))))))).
thf(conj_thm_2Ecomplex_2EMODU__POW2,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Ereal_2Epow@(ap@c_2Ecomplex_2Emodu@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Erealax_2Ereal__add@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ecomplex_2ERE@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ecomplex_2EIM@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))).
thf(conj_thm_2Ecomplex_2ERE__IM__LE__MODU,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Eabs@(ap@c_2Ecomplex_2ERE@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))))@(ap@c_2Ecomplex_2Emodu@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))) & (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Eabs@(ap@c_2Ecomplex_2EIM@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))))@(ap@c_2Ecomplex_2Emodu@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))))))).
thf(conj_thm_2Ecomplex_2EMODU__POS,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : (p@(ap@(ap@c_2Ereal_2Ereal__lte@(ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@c_2Ecomplex_2Emodu@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__MUL__RCONJ1,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(ap@c_2Ecomplex_2Econj@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__real@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ecomplex_2Emodu@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))).
thf(conj_thm_2Ecomplex_2ECOMPLEX__MUL__LCONJ1,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@(ap@c_2Ecomplex_2Ecomplex__mul@(ap@c_2Ecomplex_2Econj@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))) = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__real@(ap@(ap@c_2Ereal_2Epow@(ap@c_2Ecomplex_2Emodu@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))).
thf(conj_thm_2Ecomplex_2EMODU__NEG,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Emodu@(ap@c_2Ecomplex_2Ecomplex__neg@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Emodu@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))))).
thf(conj_thm_2Ecomplex_2EMODU__SUB,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Emodu@(ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Emodu@(ap@(ap@c_2Ecomplex_2Ecomplex__sub@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))))))).
thf(conj_thm_2Ecomplex_2EMODU__CONJ,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Emodu@(ap@c_2Ecomplex_2Econj@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Emodu@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))))).
thf(conj_thm_2Ecomplex_2EMODU__MUL,lemma,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ( ! [V1w:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Emodu@(ap@(ap@c_2Ecomplex_2Ecomplex__mul@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z))@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))) = (surj__ty_2Erealax_2Ereal @ (ap@(ap@c_2Erealax_2Ereal__mul@(ap@c_2Ecomplex_2Emodu@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))@(ap@c_2Ecomplex_2Emodu@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V1w)))))))).
thf(conj_thm_2Ecomplex_2EMODU__0,lemma,((surj__ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Emodu@(ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))).
thf(conj_thm_2Ecomplex_2EMODU__1,lemma,((surj__ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Emodu@(ap@c_2Ecomplex_2Ecomplex__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Ereal_2Ereal__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))).
thf(conj_thm_2Ecomplex_2EMODU__COMPLEX__INV,conjecture,( ! [V0z:tp__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal] : ((~~ (V0z = (surj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Ecomplex__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) => ((surj__ty_2Erealax_2Ereal @ (ap@c_2Ecomplex_2Emodu@(ap@c_2Ecomplex_2Ecomplex__inv@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))) = (surj__ty_2Erealax_2Ereal @ (ap@c_2Erealax_2Einv@(ap@c_2Ecomplex_2Emodu@(inj__c_ty_2Epair_2Eprod_ty_2Erealax_2Ereal_ty_2Erealax_2Ereal @ V0z)))))))).
