environ
vocabularies HIDDEN, TURING_1, COMPOS_1, SCMFSA6A, AMI_1, AMISTD_1, SCMPDS_5, FUNCT_1, CARD_1, ARYTM_1, NAT_1, RELAT_1, ZFMISC_1, ARYTM_3, XXREAL_0, AMISTD_2, TARSKI, XBOOLE_0, NUMBERS, FINSET_1, EXTPRO_1, FUNCOP_1, FUNCT_4, RELOC, VALUED_1, SUBSET_1, PARTFUN1, RCOMP_1, AMISTD_4, ORDINAL4, SCMFSA_7;
notations HIDDEN, TARSKI, XBOOLE_0, RELAT_1, ZFMISC_1, FUNCT_1, FUNCOP_1, ORDINAL1, SUBSET_1, FINSET_1, PARTFUN1, FUNCT_4, CARD_1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, NAT_D, VALUED_0, VALUED_1, AFINSQ_1, COMPOS_0, COMPOS_1, AMISTD_4;
definitions TARSKI, COMPOS_1, AMISTD_4;
theorems COMPOS_1, COMPOS_0, AFINSQ_1, XREAL_1, ZFMISC_1, AMISTD_4, XBOOLE_1, FUNCT_7, VALUED_1, RELAT_1, TARSKI, XBOOLE_0, FUNCT_1, GRFUNC_1, FUNCT_4, FUNCOP_1, NAT_1, XXREAL_0, ORDINAL1, PARTFUN1, XTUPLE_0;
schemes ;
registrations COMPOS_0, COMPOS_1, CARD_1, NAT_1, XREAL_0, ORDINAL1, VALUED_1, FUNCOP_1, AFINSQ_1, RELAT_1, XBOOLE_0, FINSEQ_1, VALUED_0;
constructors HIDDEN, COMPOS_1, AMISTD_4, VALUED_1, NAT_D, XXREAL_0, XREAL_0, XCMPLX_0, AMISTD_1, AMISTD_2, NAT_1, PRE_POLY, DOMAIN_1, RELSET_1, FUNCT_4;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities COMPOS_1, VALUED_1, FUNCOP_1;
expansions TARSKI, COMPOS_1;
Lm1:
for f, g being Function st f c= g holds
for x, y being set st not x in rng f holds
f c= g \ (y .--> x)