environ
vocabularies HIDDEN, NUMBERS, METRIC_1, SUBSET_1, XBOOLE_0, FUNCT_1, ZFMISC_1, REAL_1, COMPLEX1, ARYTM_1, XXREAL_0, ARYTM_3, PCOMPS_1, CARD_1, RELAT_1, RELAT_2, STRUCT_0, NAT_1, ORDINAL2, XXREAL_2, TARSKI, SEQ_2, SEQ_1, VALUED_0, BHSP_3, METRIC_6, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, DOMAIN_1, REAL_1, NAT_1, STRUCT_0, METRIC_1, SEQ_1, SEQ_2, VALUED_0, PCOMPS_1, TBSP_1, XXREAL_0, RECDEF_1;
definitions TBSP_1, TARSKI;
theorems ABSVALUE, BINOP_1, METRIC_1, FUNCT_1, FUNCT_2, SEQ_2, NAT_1, PCOMPS_1, SEQM_3, SEQ_4, TBSP_1, SUBSET_1, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, VALUED_0, ORDINAL1;
schemes SEQ_1, BINOP_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, STRUCT_0, METRIC_1, VALUED_0, FUNCT_2, TBSP_1, NAT_1;
constructors HIDDEN, DOMAIN_1, REAL_1, COMPLEX1, SEQ_2, PCOMPS_1, TBSP_1, RECDEF_1, RELSET_1, RVSUM_1, COMSEQ_2, BINOP_1, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities ;
expansions TBSP_1, TARSKI;
definition
let A be non
empty set ;
let G be
Function of
[:A,A:],
REAL;
existence
ex b1 being Function of [:A,A:],REAL st
for a, b being Element of A holds b1 . (a,b) = (G . (a,b)) / (1 + (G . (a,b)))
uniqueness
for b1, b2 being Function of [:A,A:],REAL st ( for a, b being Element of A holds b1 . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) ) & ( for a, b being Element of A holds b2 . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) ) holds
b1 = b2
end;