environ
vocabularies HIDDEN, XBOOLE_0, SUBSET_1, PARTFUN1, NUMBERS, RELAT_1, ARYTM_3, CARD_1, COMPLEX1, ORDINAL4, FUNCT_1, ARYTM_1, VALUED_1, TARSKI, XXREAL_2, XXREAL_0, FUNCT_7, REAL_1, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, RFUNCT_1, COMPLEX1, VALUED_1, COMSEQ_2, SEQ_2;
definitions TARSKI, PARTFUN1, XBOOLE_0, COMSEQ_2;
theorems TARSKI, SUBSET_1, FUNCT_1, PARTFUN1, PARTFUN2, RFUNCT_1, COMPLEX1, RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, XXREAL_0, VALUED_1, XREAL_0, FUNCT_2;
schemes PARTFUN2;
registrations RELSET_1, NUMBERS, XREAL_0, MEMBERED, VALUED_0, RFUNCT_1, XCMPLX_0;
constructors HIDDEN, PARTFUN1, XXREAL_0, REAL_1, COMPLEX1, PARTFUN2, VALUED_1, RFUNCT_1, SEQ_2, NAT_1, RELSET_1, COMSEQ_2;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities XBOOLE_0, VALUED_1;
expansions PARTFUN1, XBOOLE_0, COMSEQ_2;
Lm1:
for x, Y being set
for C being non empty set
for f being PartFunc of C,COMPLEX holds
( x in f " Y iff ( x in dom f & f /. x in Y ) )
by PARTFUN2:26;
Lm2:
(- 1r) " = - 1r
by COMPLEX1:def 4;
Lm3:
for C being non empty set
for f being PartFunc of C,COMPLEX holds
( |.f.| is bounded iff f is bounded )
::DEFINITIONS OF COMPLEX FUNCTIONS
::