environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, FUNCT_1, NAT_1, TARSKI, MEMBERED, ORDINAL1, FINSET_1, RELAT_1, AFINSQ_1, ARYTM_1, ARYTM_3, FINSEQ_1, XXREAL_0, CARD_1, XBOOLE_0, ORDINAL4, FINSEQ_5, RFINSEQ, JORDAN3, CARD_3, XCMPLX_0, AFINSQ_2, BINOP_1, SETWISEO, FINSOP_1, FUNCOP_1, BINOP_2, VALUED_0, FUNCT_2, INT_1, PRGCOR_2, XREAL_0, SEQ_1, SERIES_1, VALUED_1, RAT_1, SQUARE_1, COMPLEX1, PARTFUN3, PRE_POLY, AMISTD_1, AMISTD_2, REAL_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, XREAL_0, ORDINAL1, CARD_1, NUMBERS, RELAT_1, FUNCT_1, XCMPLX_0, NAT_1, FINSET_1, XXREAL_0, NAT_D, AFINSQ_1, SEQ_1, MEMBERED, VALUED_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, INT_1, BINOP_1, BINOP_2, SETWISEO, FINSOP_1, FINSEQ_1, RECDEF_1, VALUED_0, SERIES_1, RAT_1, PARTFUN3;
definitions TARSKI, XBOOLE_0, FUNCT_1;
theorems TARSKI, FUNCT_1, NAT_1, ZFMISC_1, RELAT_1, CARD_2, XBOOLE_0, XBOOLE_1, FINSET_1, ORDINAL1, CARD_1, XREAL_1, AFINSQ_1, XXREAL_0, NAT_2, FINSEQ_2, WELLORD2, MEMBERED, VALUED_0, VALUED_1, XREAL_0, NAT_D, SERIES_1, PARTFUN3, BINOP_1, BINOP_2, SETWISEO, FUNCOP_1, FINSOP_1, FINSEQ_1, FUNCT_2, XCMPLX_0, GRFUNC_1, RAT_1, INT_1;
schemes NAT_1, AFINSQ_1, FUNCT_2, BINOP_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, BINOP_2, CARD_1, FINSEQ_1, AFINSQ_1, RELSET_1, ORDINAL3, VALUED_1, VALUED_0, MEMBERED, FINSEQ_2;
constructors HIDDEN, SERIES_1, PARTFUN3, WELLORD2, SETWISEO, FINSOP_1, NAT_D, RECDEF_1, BINOP_2, RELSET_1, AFINSQ_1, FUNCOP_1, SQUARE_1, BINOP_1, XTUPLE_0;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities VALUED_1, BINOP_1, ORDINAL1, CARD_1;
expansions TARSKI, XBOOLE_0, FUNCT_1, BINOP_1, ORDINAL1;
Lm1:
for X, Y being finite set
for F being Function of X,Y st card X = card Y holds
( F is onto iff F is one-to-one )
definition
let X be
finite natural-membered set ;
existence
ex b1 being XFinSequence of NAT st
( rng b1 = X & ( for l, m, k1, k2 being Nat st l < m & m < len b1 & k1 = b1 . l & k2 = b1 . m holds
k1 < k2 ) )
uniqueness
for b1, b2 being XFinSequence of NAT st rng b1 = X & ( for l, m, k1, k2 being Nat st l < m & m < len b1 & k1 = b1 . l & k2 = b1 . m holds
k1 < k2 ) & rng b2 = X & ( for l, m, k1, k2 being Nat st l < m & m < len b2 & k1 = b2 . l & k2 = b2 . m holds
k1 < k2 ) holds
b1 = b2
end;
reconsider zz = 0 as Nat ;
Lm2:
for cF being complex-valued XFinSequence holds cF is COMPLEX -valued
Lm3:
for rF being real-valued XFinSequence holds rF is REAL -valued