environ
vocabularies HIDDEN, SUBSET_1, XBOOLE_0, FUNCT_1, NUMBERS, CARD_3, ORDINAL1, CARD_1, FUNCOP_1, RELAT_1, TARSKI, NAT_1, AMISTD_2, ZFMISC_1, AMI_1, ARYTM_3, RECDEF_2, FINSEQ_1, UNIALG_1, VALUED_0, SCMPDS_5, FUNCT_4, COMPOS_0, XTUPLE_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, MCART_1, SUBSET_1, SETFAM_1, ORDINAL1, PBOOLE, CARD_1, CARD_3, XXREAL_0, XCMPLX_0, RELAT_1, FUNCT_1, PARTFUN1, NUMBERS, INT_1, NAT_1, NAT_D, FUNCOP_1, FUNCT_4, FUNCT_7, FINSEQ_1, FUNCT_2, DOMAIN_1, VALUED_0, VALUED_1, RECDEF_2, AFINSQ_1, STRUCT_0;
definitions TARSKI, FUNCT_1, XBOOLE_0, VALUED_0, CARD_3;
theorems ZFMISC_1, TARSKI, CARD_3, FINSEQ_1, ENUMSET1, FUNCOP_1, FUNCT_1, XBOOLE_0, XBOOLE_1, ORDINAL1, MCART_1, RECDEF_2, VALUED_1, FUNCT_7, CHAIN_1, XTUPLE_0;
schemes ;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, FINSEQ_1, CARD_3, RELSET_1, PRE_POLY, AFINSQ_1, VALUED_1, NAT_1, CARD_1, VALUED_0, XTUPLE_0;
constructors HIDDEN, SETFAM_1, DOMAIN_1, FUNCT_4, XXREAL_0, RELSET_1, FUNCT_7, PRE_POLY, PBOOLE, AFINSQ_1, NAT_D, WELLORD2, STRUCT_0, XTUPLE_0, XFAMILY;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities ZFMISC_1, TARSKI, XTUPLE_0;
expansions TARSKI, FUNCT_1, XBOOLE_0;
Lm1:
for T being InsType of {[0,{},{}]} holds JumpParts T = {0}
Lm2:
for S being non empty standard-ins homogeneous set
for I being Element of S
for x being set st x in dom (JumpPart I) holds
(product" (JumpParts (InsCode I))) . x c= NAT
Lm3:
for S being non empty standard-ins homogeneous set st S is J/A-independent holds
for I being Element of S
for x being set st x in dom (JumpPart I) holds
NAT c= (product" (JumpParts (InsCode I))) . x
Lm4:
for T being InsType of {[0,{},{}],[1,{},{}]} holds JumpParts T = {0}
registration
coherence
( {[0,{},{}],[1,{},{}]} is J/A-independent & {[0,{},{}],[1,{},{}]} is homogeneous )
end;