environ
vocabularies HIDDEN, NUMBERS, SETFAM_1, FUNCT_1, SUBSET_1, INT_1, RELAT_1, CARD_1, XXREAL_0, ARYTM_3, ARYTM_1, FUNCT_7, XBOOLE_0, TARSKI, ZFMISC_1, FINSET_1, EQREL_1, FUNCOP_1, ABIAN, XCMPLX_0, NAT_1, RECDEF_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, MCART_1, DOMAIN_1, FINSET_1, SETFAM_1, SEQ_4, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, INT_1, NAT_1, NAT_D, EQREL_1, FUNCT_7, XXREAL_0;
definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, SETFAM_1, INT_1;
theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, EQREL_1, NAT_1, INT_1, MCART_1, SCHEME1, FUNCOP_1, SETFAM_1, XBOOLE_0, XBOOLE_1, FUNCT_7, XREAL_1, XXREAL_0, NAT_D, XXREAL_2;
schemes EQREL_1, FUNCT_2, NAT_1, DOMAIN_1;
registrations XBOOLE_0, SUBSET_1, SETFAM_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FINSET_1, XREAL_0, INT_1, MEMBERED, EQREL_1, XXREAL_2, XXREAL_0, NAT_1;
constructors HIDDEN, SETFAM_1, XXREAL_0, REAL_1, NAT_1, NAT_D, EQREL_1, SEQ_4, REALSET1, FUNCT_7, XXREAL_2, RELSET_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities RELAT_1;
expansions XBOOLE_0, INT_1;
Lm1:
for i being Integer holds
( i is even iff ex j being Integer st i = 2 * j )
by INT_1:def 3;
definition
let E be
set ;
let f be
Function of
E,
E;
existence
ex b1 being Equivalence_Relation of E st
for x, y being set st x in E & y in E holds
( [x,y] in b1 iff ex k, l being Nat st (iter (f,k)) . x = (iter (f,l)) . y )
uniqueness
for b1, b2 being Equivalence_Relation of E st ( for x, y being set st x in E & y in E holds
( [x,y] in b1 iff ex k, l being Nat st (iter (f,k)) . x = (iter (f,l)) . y ) ) & ( for x, y being set st x in E & y in E holds
( [x,y] in b2 iff ex k, l being Nat st (iter (f,k)) . x = (iter (f,l)) . y ) ) holds
b1 = b2
end;
theorem
for
n being
Nat holds
(
n is
odd iff ex
k being
Nat st
n = (2 * k) + 1 )