environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, FUNCT_1, RELAT_1, TARSKI, XBOOLE_0, FUNCOP_1, PBOOLE, ZFMISC_1, FUNCT_4, FINSEQ_1, ARYTM_3, CARD_1, NAT_1, XXREAL_0, FINSET_1, SETFAM_1, FINSEQ_2, ORDINAL4, MCART_1, PARTFUN1, REWRITE1, FUNCT_2, ARYTM_1, RFINSEQ, CLASSES1, FUNCT_7, VALUED_1, ORDINAL1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, XTUPLE_0, SUBSET_1, CARD_1, WELLORD2, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, SETFAM_1, PBOOLE, DOMAIN_1, RELAT_1, FUNCT_1, RELSET_1, BINOP_1, FINSET_1, PARTFUN1, FUNCOP_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FUNCT_4, CLASSES1, RFINSEQ, NAT_D, REWRITE1, VALUED_1;
definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, FUNCOP_1;
theorems FINSEQ_1, RELAT_1, TARSKI, AXIOMS, ZFMISC_1, INT_1, FUNCT_1, FINSEQ_2, FUNCT_4, SUBSET_1, FINSET_1, CARD_1, NAT_1, FUNCT_2, FUNCOP_1, SETFAM_1, FINSEQ_3, ENUMSET1, REWRITE1, FINSEQ_4, RELSET_1, XBOOLE_0, XBOOLE_1, PARTFUN1, GRFUNC_1, XREAL_1, XXREAL_0, ORDINAL1, RFINSEQ, FINSEQ_5, NAT_D, WELLORD2, VALUED_1, XTUPLE_0;
schemes NAT_1, DOMAIN_1, CLASSES1, FRAENKEL, FINSEQ_1, RECDEF_1, FUNCT_2;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1, FUNCOP_1, FUNCT_4, XREAL_0, NAT_1, INT_1, CARD_1, FINSEQ_1, FUNCT_2, RELSET_1, XXREAL_0, XTUPLE_0, FINSEQ_3;
constructors HIDDEN, SETFAM_1, PARTFUN1, WELLORD2, BINOP_1, DOMAIN_1, FUNCT_4, XXREAL_0, NAT_1, INT_1, PBOOLE, RFINSEQ, NAT_D, REWRITE1, RELAT_2, REAL_1, CLASSES1, RELSET_1, VALUED_1, FINSEQ_2, XTUPLE_0;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities TARSKI, RELAT_1, FUNCOP_1, BINOP_1, FINSEQ_2, FUNCT_4, ORDINAL1;
expansions TARSKI, XBOOLE_0, FUNCT_1, FUNCOP_1;
theorem
for
A,
B being
set st
A * c= B * holds
A c= B
Lm1:
for X being set
for f being Function of X,X holds rng f c= dom f
Lm2:
for f being Relation
for n being Nat
for p1, p2 being sequence of (bool [:(field f),(field f):]) st p1 . 0 = id (field f) & ( for k being Nat holds p1 . (k + 1) = f * (p1 . k) ) & p2 . 0 = id (field f) & ( for k being Nat holds p2 . (k + 1) = f * (p2 . k) ) holds
p1 = p2
Lm3:
for R being Relation holds
( (id (field R)) * R = R & R * (id (field R)) = R )
by RELAT_1:51, RELAT_1:53, XBOOLE_1:7;
Lm4:
for R being Relation st rng R c= dom R holds
iter (R,0) = id (dom R)
Lm5:
for m, k being Nat
for R being Relation st iter ((iter (R,m)),k) = iter (R,(m * k)) holds
iter ((iter (R,m)),(k + 1)) = iter (R,(m * (k + 1)))