environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, FUNCT_1, ARYTM_3, XXREAL_0, XBOOLE_0, TARSKI, NAT_1, ORDINAL1, FINSEQ_1, CARD_1, FINSET_1, RELAT_1, PARTFUN1, FUNCOP_1, ORDINAL4, ORDINAL2, ARYTM_1, REAL_1, ZFMISC_1, FUNCT_4, VALUED_0, AFINSQ_1, PRGCOR_2, CAT_1, AMISTD_1, AMISTD_3, AMISTD_2, VALUED_1, CONNSP_3;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, CARD_1, ORDINAL2, NUMBERS, ORDINAL4, XCMPLX_0, XREAL_0, NAT_1, PARTFUN1, BINOP_1, FINSOP_1, NAT_D, FINSET_1, FINSEQ_1, FUNCOP_1, FUNCT_4, FUNCT_7, XXREAL_0, VALUED_0, VALUED_1;
definitions TARSKI, ORDINAL1, XBOOLE_0, RELAT_1, PARTFUN1, CARD_1, FUNCT_1;
theorems TARSKI, AXIOMS, FUNCT_1, NAT_1, ZFMISC_1, RELAT_1, RELSET_1, ORDINAL1, CARD_1, FINSEQ_1, FUNCT_7, ORDINAL4, CARD_2, FUNCT_4, ORDINAL3, XBOOLE_0, XBOOLE_1, FINSET_1, FUNCOP_1, XREAL_1, VALUED_0, ENUMSET1, XXREAL_0, XREAL_0, GRFUNC_1, XXREAL_2, NAT_D, VALUED_1, XTUPLE_0;
schemes FUNCT_1, SUBSET_1, NAT_1, XBOOLE_0, CLASSES1, FINSEQ_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, XXREAL_0, XREAL_0, NAT_1, CARD_1, ORDINAL2, NUMBERS, VALUED_1, XXREAL_2, MEMBERED, FINSET_1, FUNCT_4;
constructors HIDDEN, WELLORD2, FUNCT_4, XXREAL_0, ORDINAL4, FUNCT_7, ORDINAL3, VALUED_1, ENUMSET1, NAT_D, XXREAL_2, BINOP_1, FINSOP_1, RELSET_1, CARD_1, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities ORDINAL1, FUNCOP_1, VALUED_1, NAT_1, CARD_1;
expansions TARSKI, ORDINAL1, XBOOLE_0, RELAT_1, CARD_1, FUNCT_1;
Lm1:
for k being Nat
for p being XFinSequence holds
( k < len p iff k in dom p )
Lm2:
for x, y being object
for x1, y1 being set st [x,y] in {[x1,y1]} holds
( x = x1 & y = y1 )
Lm3:
for x1, x2, x3, x4 being object holds
( <%x1,x2,x3,x4%> . 1 = x2 & <%x1,x2,x3,x4%> . 2 = x3 & <%x1,x2,x3,x4%> . 3 = x4 )
registration
let x1,
x2,
x3,
x4 be
object ;
reducibility
<%x1,x2,x3,x4%> . 0 = x1
reducibility
<%x1,x2,x3,x4%> . 1 = x2
by Lm3;
reducibility
<%x1,x2,x3,x4%> . 2 = x3
by Lm3;
reducibility
<%x1,x2,x3,x4%> . 3 = x4
by Lm3;
end;
::$CT