environ
vocabularies HIDDEN, NUMBERS, FINSEQ_1, CARD_1, XXREAL_0, RELAT_1, REAL_1, FUNCT_1, ARYTM_3, FUNCOP_1, ARYTM_1, RFINSEQ, CLASSES1, FUNCT_2, XBOOLE_0, VALUED_0, ORDINAL4, NAT_1, RFINSEQ2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XXREAL_0, RELAT_1, XCMPLX_0, XREAL_0, FUNCT_1, FUNCT_2, FINSEQ_1, REAL_1, NAT_1, RVSUM_1, FUNCOP_1, CLASSES1, RFINSEQ, INTEGRA2;
definitions INTEGRA2;
theorems TARSKI, FINSEQ_1, FINSEQ_2, FINSEQ_3, NAT_1, FUNCT_1, FUNCT_2, RVSUM_1, RELAT_1, FUNCOP_1, RFINSEQ, INTEGRA2, XREAL_1, XXREAL_0, VALUED_1, CLASSES1;
schemes NAT_1;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, NAT_1, MEMBERED, FINSEQ_1, INTEGRA2, VALUED_0, FINSET_1, CARD_1, XREAL_0, ORDINAL1;
constructors HIDDEN, FUNCOP_1, REAL_1, NAT_1, BINOP_2, SEQM_3, RFINSEQ, INTEGRA2, RVSUM_1, CLASSES1, RELSET_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities RELAT_1;
expansions INTEGRA2;
Lm1:
for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent holds
max f <= max g
Lm2:
for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent holds
min f >= min g
Lm3:
for f, g being non-decreasing FinSequence of REAL
for n being Nat st len f = n + 1 & len f = len g & f,g are_fiberwise_equipotent holds
( f . (len f) = g . (len g) & f | n,g | n are_fiberwise_equipotent )
Lm4:
for n being Nat
for g1, g2 being non-decreasing FinSequence of REAL st n = len g1 & g1,g2 are_fiberwise_equipotent holds
g1 = g2