environ
vocabularies HIDDEN, STRUCT_0, ALGSTR_0, NUMBERS, BINOP_2, MESFUNC1, COMPLEX1, SUPINF_2, XBOOLE_0, XCMPLX_0, SUBSET_1, ORDINAL1, ARYTM_3, FUNCT_1, RELAT_1, VECTSP_1, GROUP_1, RLVECT_1, BINOP_1, LATTICES, ARYTM_1, CARD_1, XXREAL_0, NAT_1, NEWTON, COMPTRIG, COMPLFLD, MEMBERED;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1, REAL_1, NAT_1, MEMBERED, FUNCT_1, XXREAL_0, COMPTRIG, BINOP_1, BINOP_2, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, NEWTON, VECTSP_1;
definitions RLVECT_1, GROUP_1, VECTSP_1, COMPTRIG, ALGSTR_0;
theorems COMPLEX1, RLVECT_1, VECTSP_1, XCMPLX_0, XCMPLX_1, BINOP_2, GROUP_1, COMPTRIG, NEWTON, ORDINAL1, NAT_1, XREAL_1;
schemes NAT_1;
registrations ORDINAL1, RELSET_1, NUMBERS, XCMPLX_0, NAT_1, COMPLEX1, STRUCT_0, VECTSP_1, XREAL_0, CARD_1, MEMBERED;
constructors HIDDEN, BINOP_1, XXREAL_0, REAL_1, NAT_1, BINOP_2, NEWTON, COMPTRIG, VECTSP_1, RLVECT_1, GROUP_1, MEMBERED;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities VECTSP_1, BINOP_1, STRUCT_0, COMPLEX1, ALGSTR_0;
expansions RLVECT_1, GROUP_1, VECTSP_1, STRUCT_0;
Lm1:
1_ F_Complex = 1r
by Def1;
Lm2:
1. F_Complex = 1r
by Def1;