environ
vocabularies HIDDEN, NUMBERS, ABIAN, RELAT_1, CARD_1, ARYTM_3, ORDERS_2, SUBSET_1, TARSKI, ZFMISC_1, FUNCT_1, XXREAL_0, FINSET_1, XBOOLE_0, FINSEQ_1, MCART_1, LATTICES, LATTICE3, PBOOLE, EQREL_1, FINSUB_1, PARTFUN1, HEYTING1, SUBSTLAT, NORMFORM, REALSET1, STRUCT_0, BINOP_1, RELAT_2, ORDINAL4, CAT_1, YELLOW_0, WELLORD1, HEYTING2, REWRITE1, HEYTING3, XCMPLX_0, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1, ORDERS_2, MEMBERED, XCMPLX_0, NAT_1, FINSEQ_1, BINOP_1, FINSET_1, FINSUB_1, PARTFUN1, LATTICES, DOMAIN_1, REALSET1, STRUCT_0, SUBSTLAT, XTUPLE_0, MCART_1, WELLORD1, YELLOW_0, ABIAN, XXREAL_2, LATTICE3, HEYTING2, XXREAL_0;
definitions TARSKI, LATTICE3, FUNCT_1, XBOOLE_0;
theorems HEYTING2, ZFMISC_1, PARTFUN1, YELLOW_0, LATTICE3, TARSKI, NAT_1, LATTICE5, FINSEQ_1, FUNCT_5, ORDERS_2, YELLOW_5, SUBSTLAT, FINSUB_1, WAYBEL15, LATTICES, GRFUNC_1, RELAT_1, SYSREL, BINOP_1, FUNCT_1, FUNCT_2, XBOOLE_0, XBOOLE_1, ORDINAL1, XREAL_1, XXREAL_0, XXREAL_2, PRE_POLY, ABIAN, XTUPLE_0;
schemes LMOD_7, XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, PARTFUN1, FINSET_1, FINSUB_1, XXREAL_0, NAT_1, MEMBERED, FINSEQ_1, REALSET1, ABIAN, STRUCT_0, LATTICES, LATTICE3, YELLOW_0, YELLOW_1, SUBSTLAT, XXREAL_2, RELAT_1, HEYTING2, XTUPLE_0, XCMPLX_0;
constructors HIDDEN, BINOP_1, TOLER_1, REALSET1, ABIAN, LATTICE3, YELLOW_0, HEYTING2, VALUED_1, XXREAL_2, RELSET_1, XTUPLE_0, XXREAL_1;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS, REAL, ARITHM;
equalities LATTICE3, BINOP_1, REALSET1, WELLORD1;
expansions TARSKI, LATTICE3, XBOOLE_0;
Lm1:
for A, x being set holds [:A,{x}:] is Function
Lm2:
0 = 2 * 0
;
Lm3:
1 = 0 + 1
;
definition
let n,
k be
Nat;
existence
ex b1 being Element of PFuncs (NAT,{k}) st
for x being object holds
( x in b1 iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) )
uniqueness
for b1, b2 being Element of PFuncs (NAT,{k}) st ( for x being object holds
( x in b1 iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) ) ) & ( for x being object holds
( x in b2 iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) ) ) holds
b1 = b2
end;
Lm4:
for n being Element of NAT holds (2 * n) + 1 <= (2 * (n + 1)) + 1
Lm5:
for n, n9 being Element of NAT holds not PFCrt ((n + 1),n9) c= PFCrt (n,n9)
Lm6:
for n, k being Element of NAT holds PFCrt (n,k) c= PFCrt ((n + 1),k)
Lm7:
for n, m, k being Element of NAT st n < k holds
PFCrt (n,m) c= PFArt (k,m)
definition
let n,
k be
Nat;
existence
ex b1 being Element of Fin (PFuncs (NAT,{k})) st
for x being object holds
( x in b1 iff ( ex m being non zero Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) )
uniqueness
for b1, b2 being Element of Fin (PFuncs (NAT,{k})) st ( for x being object holds
( x in b1 iff ( ex m being non zero Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) ) ) & ( for x being object holds
( x in b2 iff ( ex m being non zero Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) ) ) holds
b1 = b2
end;
Lm8:
for n, k being Element of NAT
for x being set st x in PFBrt (n,k) holds
x is finite
Lm9:
for a being non empty set st a <> {{}} & {} in a holds
ex b being set st
( b in a & b <> {} )
Lm10:
for m being Element of NAT holds not SubstPoset (NAT,{m}) is complete