environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, PROB_1, MEASURE1, PARTFUN1, SUBSET_1, RELAT_1, FUNCT_1, XXREAL_0, ARYTM_1, SUPINF_2, SUPINF_1, CARD_1, REAL_1, VALUED_1, INTEGRA5, MESFUNC5, ARYTM_3, MESFUNC1, COMPLEX1, TARSKI, MESFUNC2, VALUED_0, FINSEQ_1, BINOP_1, SETWISEO, CARD_3, FINSEQ_2, NEWTON, ORDINAL4, NAT_1, POWER, SQUARE_1, XXREAL_2, ORDINAL2, RFUNCT_3, FUNCT_3, MESFUNC7, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, VALUED_0, XXREAL_3, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, XXREAL_0, XXREAL_2, MEASURE1, NAT_1, SUPINF_1, RELAT_1, RELSET_1, SETWISEO, PARTFUN1, FUNCT_1, FINSEQ_1, FINSEQ_2, SETWOP_2, BINOP_1, FUNCT_2, NEWTON, SQUARE_1, PROB_1, SUPINF_2, EXTREAL1, POWER, MESFUNC5, MESFUNC1, MESFUNC2, MEASURE6;
definitions TARSKI;
theorems ABSVALUE, SETWISEO, POWER, HOLDER_1, TARSKI, PARTFUN1, FUNCT_1, SUPINF_2, EXTREAL1, BINOP_1, MESFUNC1, FINSEQ_1, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_1, MESFUNC2, NEWTON, XREAL_1, COMPLEX1, XXREAL_0, FINSEQ_2, MESFUNC5, FINSOP_1, NAT_1, RELAT_1, FUNCT_3, MEASURE1, MESFUNC6, ORDINAL1, VALUED_0, XXREAL_2, XXREAL_3;
schemes FUNCT_2, NAT_1, PARTFUN2, BINOP_1, BINOP_2;
registrations SUBSET_1, NAT_1, RELSET_1, XREAL_0, MEMBERED, ORDINAL1, FINSEQ_1, MEASURE1, NUMBERS, XXREAL_0, XBOOLE_0, VALUED_0, POWER, XXREAL_3, SQUARE_1, NEWTON, CARD_1;
constructors HIDDEN, REAL_1, FINSOP_1, EXTREAL1, BINOP_1, NEWTON, POWER, MESFUNC1, MEASURE6, MESFUNC2, MEASURE3, SETWISEO, SQUARE_1, MESFUNC5, SUPINF_1, RELSET_1, BINOP_2, FINSEQ_2;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities MESFUNC1, MESFUNC5, XCMPLX_0, SQUARE_1, SUPINF_2;
expansions TARSKI, MESFUNC1, MESFUNC5;
reconsider jj = 1 as Real ;
Lm1:
1. is_a_unity_wrt multextreal