environ
vocabularies HIDDEN, SUBSET_1, STRUCT_0, NORMSP_1, FUNCT_1, NUMBERS, REAL_1, XBOOLE_0, FUNCT_5, CARD_1, METRIC_1, RELAT_2, SUPINF_2, XCMPLX_0, NAT_1, SEQ_1, RELAT_1, TARSKI, PARTFUN1, NORMSP_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, FUNCT_5, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1, SEQ_1, STRUCT_0;
definitions TARSKI, RELAT_1, FUNCT_1;
theorems FUNCOP_1, TARSKI, FUNCT_1, RELAT_1, RELSET_1, PARTFUN1, FUNCT_2, STRUCT_0, XREAL_0, ORDINAL1;
schemes FUNCT_1;
registrations STRUCT_0, RELSET_1, XBOOLE_0, NUMBERS, XREAL_0, ORDINAL1, FUNCT_2;
constructors HIDDEN, FUNCT_2, NUMBERS, STRUCT_0, FUNCT_5, FUNCOP_1, XCMPLX_0, RELSET_1, XREAL_0;
requirements HIDDEN, BOOLE, SUBSET;
equalities FUNCT_5, FUNCOP_1, STRUCT_0;
expansions ;
0 in REAL
by XREAL_0:def 1;
then reconsider f = op1 as Function of {0},REAL by FUNCOP_1:46;
reconsider z = 0 as Element of {0} by TARSKI:def 1;