:: ABIAN semantic presentation

begin


definition
let i be Integer;
attri is even  means :Def1: :: ABIAN:def 1
2 divides i;
end;

:: deftheorem Def1 defines even ABIAN:def_1_:_
 for i being Integer holds
( i is even iff 2 divides i );

notation
let i be Integer;
antonym  odd i for  even ;
end;

Lm1:  for i being Integer holds
( i is even iff ex j being Integer st i = 2 * j )
proof
let i be Integer; ::_thesis: ( i is even iff ex j being Integer st i = 2 * j )
hereby  ::_thesis: ( ex j being Integer st i = 2 * j implies i is even )
assume  i is even ; ::_thesis: ex j being Integer st i = 2 * j
then  2 divides i by Def1;
hence  ex j being Integer st i = 2 * j by INT_1:def_3; ::_thesis: verum
end;
assume  ex j being Integer st i = 2 * j ; ::_thesis: i is even
hence  2 divides i by INT_1:def_3; :: according to ABIAN:def_1 ::_thesis: verum
end;

definition
let n be Element of NAT ;
redefine attr n is even  means :: ABIAN:def 2
 ex k being Element of NAT st n = 2 * k;
compatibility
 ( n is even iff ex k being Element of NAT st n = 2 * k )
proof
hereby  ::_thesis: ( ex k being Element of NAT st n = 2 * k implies n is even )
assume  n is even ; ::_thesis: ex k being Element of NAT st n = 2 * k
then  2 divides n by Def1;
then consider k being Integer such that
A1: n = 2 * k by INT_1:def_3;
 0 <= k by A1, NAT_1:2, XREAL_1:132;
then reconsider k = k as Element of NAT by INT_1:3;
take k = k; ::_thesis: n = 2 * k
thus  n = 2 * k by A1; ::_thesis: verum
end;
thus  ( ex k being Element of NAT st n = 2 * k implies n is even ) by Lm1; ::_thesis: verum
end;
end;

:: deftheorem  defines even ABIAN:def_2_:_
 for n being Element of NAT holds
( n is even iff ex k being Element of NAT st n = 2 * k );

registration
cluster ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() even for Element of NAT ;
existence
 ex b1 being Element of NAT st b1 is even
proof
take  0 ; ::_thesis: 0 is even
take  0 ; :: according to ABIAN:def_2 ::_thesis: 0 = 2 * 0
thus  0 = 2 * 0 ; ::_thesis: verum
end;
cluster ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() odd for Element of NAT ;
existence
 ex b1 being Element of NAT st b1 is odd
proof
take  1 ; ::_thesis: 1 is odd
let k be Element of NAT ; :: according to ABIAN:def_2 ::_thesis: not 1 = 2 * k
thus  not 1 = 2 * k by NAT_1:15; ::_thesis: verum
end;
cluster ext-real complex V18() integer even for set ;
existence
 ex b1 being Integer st b1 is even
proof
take  0 ; ::_thesis: 0 is even
take  0 ; :: according to ABIAN:def_2 ::_thesis: 0 = 2 * 0
thus  0 = 2 * 0 ; ::_thesis: verum
end;
cluster ext-real complex V18() integer odd for set ;
existence
 ex b1 being Integer st b1 is odd
proof
take  1 ; ::_thesis: 1 is odd
assume  1 is even ; ::_thesis: contradiction
then  ex k being Integer st 1 = 2 * k by Lm1;
hence  contradiction by INT_1:9; ::_thesis: verum
end;
end;

theorem Th1: :: ABIAN:1
for i being Integer holds
( i is odd iff ex j being Integer st i = (2 * j) + 1 )
proof
let i be Integer; ::_thesis: ( i is odd iff ex j being Integer st i = (2 * j) + 1 )
hereby  ::_thesis: ( ex j being Integer st i = (2 * j) + 1 implies i is odd )
consider k being Element of NAT  such that
A1: ( i = k or i = - k ) by INT_1:2;
consider m being Element of NAT  such that
A2: ( k = 2 * m or k = (2 * m) + 1 ) by SCHEME1:1;
assume A3: i is odd ; ::_thesis: not  for j being Integer holds i <> (2 * j) + 1
assume A4: for j being Integer holds i <> (2 * j) + 1 ; ::_thesis: contradiction
percases ( ( i = k & k = 2 * m ) or ( i = - k & k = 2 * m ) or ( i = k & k = (2 * m) + 1 ) or ( i = - k & k = (2 * m) + 1 ) ) by A1, A2;
suppose ( i = k & k = 2 * m ) ; ::_thesis: contradiction
hence  contradiction by A3, Lm1; ::_thesis: verum
end;
suppose ( i = - k & k = 2 * m ) ; ::_thesis: contradiction
then  i = 2 * (- m) ;
hence  contradiction by A3, Lm1; ::_thesis: verum
end;
suppose ( i = k & k = (2 * m) + 1 ) ; ::_thesis: contradiction
hence  contradiction by A4; ::_thesis: verum
end;
suppose ( i = - k & k = (2 * m) + 1 ) ; ::_thesis: contradiction
then  i = (2 * (- (m + 1))) + 1 ;
hence  contradiction by A4; ::_thesis: verum
end;
end;
end;
given j being Integer such that A5: i = (2 * j) + 1 ; ::_thesis: i is odd
given k being Integer such that A6: i = 2 * k ; :: according to INT_1:def_3,ABIAN:def_1 ::_thesis: contradiction
 1 = 2 * (k - j) by A5, A6;
hence  contradiction by INT_1:9; ::_thesis: verum
end;

registration
let i be Integer;
cluster2 * i ->  even ;
coherence
 2 * i is even by Lm1;
end;

registration
let i be even Integer;
clusteri + 1 ->  odd ;
coherence
 not i + 1 is even
proof
 ex j being Integer st i = 2 * j by Lm1;
hence  not i + 1 is even by Th1; ::_thesis: verum
end;
end;

registration
let i be odd Integer;
clusteri + 1 ->  even ;
coherence
 i + 1 is even
proof
consider j being Integer such that
A1: i = (2 * j) + 1 by Th1;
 i + 1 = 2 * (j + 1) by A1;
hence  i + 1 is even ; ::_thesis: verum
end;
end;

registration
let i be even Integer;
clusteri - 1 ->  odd ;
coherence
 not i - 1 is even
proof
consider j being Integer such that
A1: i = 2 * j by Lm1;
 i - 1 = (2 * (j - 1)) + 1 by A1;
hence  not i - 1 is even ; ::_thesis: verum
end;
end;

registration
let i be odd Integer;
clusteri - 1 ->  even ;
coherence
 i - 1 is even
proof
 ex j being Integer st i = (2 * j) + 1 by Th1;
hence  i - 1 is even ; ::_thesis: verum
end;
end;

registration
let i be even Integer;
let j be Integer;
clusteri * j ->  even ;
coherence
 i * j is even
proof
consider k being Integer such that
A1: i = 2 * k by Lm1;
 i * j = 2 * (k * j) by A1;
hence  i * j is even ; ::_thesis: verum
end;
clusterj * i ->  even ;
coherence
 j * i is even ;
end;

registration
let i, j be odd Integer;
clusteri * j ->  odd ;
coherence
 not i * j is even
proof
consider l being Integer such that
A1: j = (2 * l) + 1 by Th1;
consider k being Integer such that
A2: i = (2 * k) + 1 by Th1;
 i * j = (2 * (((k * (2 * l)) + (k * 1)) + (l * 1))) + 1 by A2, A1;
hence  not i * j is even ; ::_thesis: verum
end;
end;

registration
let i, j be even Integer;
clusteri + j ->  even ;
coherence
 i + j is even
proof
consider l being Integer such that
A1: j = 2 * l by Lm1;
consider k being Integer such that
A2: i = 2 * k by Lm1;
 i + j = 2 * (k + l) by A2, A1;
hence  i + j is even ; ::_thesis: verum
end;
end;

registration
let i be even Integer;
let j be odd Integer;
clusteri + j ->  odd ;
coherence
 not i + j is even
proof
consider l being Integer such that
A1: j = (2 * l) + 1 by Th1;
consider k being Integer such that
A2: i = 2 * k by Lm1;
 i + j = (2 * (k + l)) + 1 by A2, A1;
hence  not i + j is even ; ::_thesis: verum
end;
clusterj + i ->  odd ;
coherence
 not j + i is even ;
end;

registration
let i, j be odd Integer;
clusteri + j ->  even ;
coherence
 i + j is even
proof
consider l being Integer such that
A1: j = (2 * l) + 1 by Th1;
consider k being Integer such that
A2: i = (2 * k) + 1 by Th1;
 j + i = 2 * ((k + l) + 1) by A2, A1;
hence  i + j is even ; ::_thesis: verum
end;
end;

registration
let i be even Integer;
let j be odd Integer;
clusteri - j ->  odd ;
coherence
 not i - j is even
proof
consider l being Integer such that
A1: j = (2 * l) + 1 by Th1;
consider k being Integer such that
A2: i = 2 * k by Lm1;
 i - j = (2 * (k - l)) - 1 by A2, A1;
hence  not i - j is even ; ::_thesis: verum
end;
clusterj - i ->  odd ;
coherence
 not j - i is even
proof
consider l being Integer such that
A3: j = (2 * l) + 1 by Th1;
consider k being Integer such that
A4: i = 2 * k by Lm1;
 j - i = (2 * (l - k)) + 1 by A4, A3;
hence  not j - i is even ; ::_thesis: verum
end;
end;

registration
let i, j be odd Integer;
clusteri - j ->  even ;
coherence
 i - j is even
proof
consider l being Integer such that
A1: j = (2 * l) + 1 by Th1;
consider k being Integer such that
A2: i = (2 * k) + 1 by Th1;
 i - j = 2 * (k - l) by A2, A1;
hence  i - j is even ; ::_thesis: verum
end;
end;

registration
let m be even Integer;
clusterm + 2 ->  even ;
coherence
 m + 2 is even
proof
 2 = 2 * 1 ;
then reconsider t = 2 as even Integer ;
 m + t is even ;
hence  m + 2 is even ; ::_thesis: verum
end;
end;

registration
let m be odd Integer;
clusterm + 2 ->  odd ;
coherence
 not m + 2 is even
proof
 2 = 2 * 1 ;
then reconsider t = 2 as even Integer ;
 m + t is odd ;
hence  not m + 2 is even ; ::_thesis: verum
end;
end;

definition
let E be set ;
let f be Function of E,E;
let n be Element of NAT ;
:: original: iter
redefine func iter (f,n) ->  Function of E,E;
coherence
 iter (f,n) is Function of E,E by FUNCT_7:83;
end;

theorem Th2: :: ABIAN:2
for S being non empty Subset of NAT st 0 in S holds
min S = 0
proof
let S be non empty Subset of NAT; ::_thesis: ( 0 in S implies min S = 0 )
assume  0 in S ; ::_thesis: min S = 0
then  min S <= 0 by XXREAL_2:def_7;
hence  min S = 0 by NAT_1:3; ::_thesis: verum
end;

theorem Th3: :: ABIAN:3
for E being non empty set
for f being Function of E,E
for x being Element of E holds (iter (f,0)) . x = x
proof
let E be non empty set ; ::_thesis: for f being Function of E,E
for x being Element of E holds (iter (f,0)) . x = x
let f be Function of E,E; ::_thesis: for x being Element of E holds (iter (f,0)) . x = x
let x be Element of E; ::_thesis: (iter (f,0)) . x = x
 dom f = E by FUNCT_2:def_1;
then A1: x in (dom f) \/ (rng f) by XBOOLE_0:def_3;
thus (iter (f,0)) . x = (id (field f)) . x by FUNCT_7:68
.= x by A1, FUNCT_1:17 ; ::_thesis: verum
end;

definition
let x be set ;
let f be Function;
predx is_a_fixpoint_of f means :Def3: :: ABIAN:def 3
( x in dom f & x = f . x );
end;

:: deftheorem Def3 defines is_a_fixpoint_of ABIAN:def_3_:_
 for x being set
for f being Function holds
( x is_a_fixpoint_of f iff ( x in dom f & x = f . x ) );

definition
let A be non empty set ;
let a be Element of A;
let f be Function of A,A;
:: original: is_a_fixpoint_of
redefine preda is_a_fixpoint_of f means :Def4: :: ABIAN:def 4
a = f . a;
compatibility
 ( a is_a_fixpoint_of f iff a = f . a )
proof
thus  ( a is_a_fixpoint_of f implies a = f . a ) by Def3; ::_thesis: ( a = f . a implies a is_a_fixpoint_of f )
assume A1: a = f . a ; ::_thesis: a is_a_fixpoint_of f
 a in A ;
hence  a in dom f by FUNCT_2:52; :: according to ABIAN:def_3 ::_thesis: a = f . a
thus  a = f . a by A1; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines is_a_fixpoint_of ABIAN:def_4_:_
 for A being non empty set
for a being Element of A
for f being Function of A,A holds
( a is_a_fixpoint_of f iff a = f . a );

definition
let f be Function;
attrf is with_fixpoint  means :Def5: :: ABIAN:def 5
 ex x being set st x is_a_fixpoint_of f;
end;

:: deftheorem Def5 defines with_fixpoint ABIAN:def_5_:_
 for f being Function holds
( f is with_fixpoint iff ex x being set st x is_a_fixpoint_of f );

notation
let f be Function;
antonym  without_fixpoints f for  with_fixpoint ;
end;

definition
let X be set ;
let x be Element of X;
attrx is covering  means :Def6: :: ABIAN:def 6
 union x = union (union X);
end;

:: deftheorem Def6 defines covering ABIAN:def_6_:_
 for X being set
for x being Element of X holds
( x is covering iff union x = union (union X) );

theorem Th4: :: ABIAN:4
for E being set
for sE being Subset-Family of E holds
( sE is covering iff union sE = E )
proof
let E be set ; ::_thesis: for sE being Subset-Family of E holds
( sE is covering iff union sE = E )
let sE be Subset-Family of E; ::_thesis: ( sE is covering iff union sE = E )
union (union (bool (bool E))) = union (bool E) by ZFMISC_1:81
.= E by ZFMISC_1:81 ;
hence  ( sE is covering iff union sE = E ) by Def6; ::_thesis: verum
end;

registration
let E be set ;
cluster non empty finite covering for Element of bool (bool E);
existence
 ex b1 being Subset-Family of E st
( not b1 is empty & b1 is finite & b1 is covering )
proof
reconsider sE = {E} as Subset-Family of E by ZFMISC_1:68;
take  sE ; ::_thesis: ( not sE is empty & sE is finite & sE is covering )
thus  ( not sE is empty & sE is finite ) ; ::_thesis: sE is covering
 union sE = E by ZFMISC_1:25;
hence  sE is covering by Th4; ::_thesis: verum
end;
end;

theorem :: ABIAN:5
for E being set
for f being Function of E,E
for sE being non empty covering Subset-Family of E st ( for X being Element of sE holds X misses f .: X ) holds
f is without_fixpoints
proof
let E be set ; ::_thesis: for f being Function of E,E
for sE being non empty covering Subset-Family of E st ( for X being Element of sE holds X misses f .: X ) holds
f is without_fixpoints
let f be Function of E,E; ::_thesis: for sE being non empty covering Subset-Family of E st ( for X being Element of sE holds X misses f .: X ) holds
f is without_fixpoints
let sE be non empty covering Subset-Family of E; ::_thesis: ( ( for X being Element of sE holds X misses f .: X ) implies f is without_fixpoints )
assume A1: for X being Element of sE holds X misses f .: X ; ::_thesis: f is without_fixpoints
given x being set  such that A2: x is_a_fixpoint_of f ; :: according to ABIAN:def_5 ::_thesis: contradiction
A3: f . x = x by A2, Def3;
A4: x in dom f by A2, Def3;
 dom f = E by FUNCT_2:52;
then  x in union sE by A4, Th4;
then consider X being set  such that
A5: x in X and
A6: X in sE by TARSKI:def_4;
 f . x in f .: X by A4, A5, FUNCT_1:def_6;
then  X meets f .: X by A3, A5, XBOOLE_0:3;
hence  contradiction by A1, A6; ::_thesis: verum
end;

definition
let E be set ;
let f be Function of E,E;
func =_ f ->  Equivalence_Relation of E means :Def7: :: ABIAN:def 7
 for x, y being set st x in E & y in E holds
( [x,y] in it iff ex k, l being Element of NAT st (iter (f,k)) . x = (iter (f,l)) . y );
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 Element of NAT st (iter (f,k)) . x = (iter (f,l)) . y )
proof
defpred S1[ set , set ] means ( $1 in E & $2 in E & ex k, l being Element of NAT st (iter (f,k)) . $1 = (iter (f,l)) . $2 );
A1: now__::_thesis:_for_x_being_set_st_x_in_E_holds_
S1[x,x]
let x be set ; ::_thesis: ( x in E implies S1[x,x] )
A2: (iter (f,0)) . x = (iter (f,0)) . x ;
assume  x in E ; ::_thesis: S1[x,x]
hence  S1[x,x] by A2; ::_thesis: verum
end;
A3: now__::_thesis:_for_x,_y,_z_being_set_st_S1[x,y]_&_S1[y,z]_holds_
S1[x,z]
let x, y, z be set ; ::_thesis: ( S1[x,y] & S1[y,z] implies S1[x,z] )
assume that
A4: S1[x,y] and
A5: S1[y,z] ; ::_thesis: S1[x,z]
consider k, l being Element of NAT  such that
A6: (iter (f,k)) . x = (iter (f,l)) . y by A4;
consider m, n being Element of NAT  such that
A7: (iter (f,m)) . y = (iter (f,n)) . z by A5;
A8: dom (iter (f,m)) = E by FUNCT_2:52;
A9: dom (iter (f,l)) = E by FUNCT_2:52;
A10: dom (iter (f,k)) = E by FUNCT_2:52;
A11: dom (iter (f,n)) = E by FUNCT_2:52;
(iter (f,(k + m))) . x = ((iter (f,m)) * (iter (f,k))) . x by FUNCT_7:77
.= (iter (f,m)) . ((iter (f,l)) . y) by A4, A6, A10, FUNCT_1:13
.= ((iter (f,m)) * (iter (f,l))) . y by A4, A9, FUNCT_1:13
.= (iter (f,(m + l))) . y by FUNCT_7:77
.= ((iter (f,l)) * (iter (f,m))) . y by FUNCT_7:77
.= (iter (f,l)) . ((iter (f,n)) . z) by A4, A7, A8, FUNCT_1:13
.= ((iter (f,l)) * (iter (f,n))) . z by A5, A11, FUNCT_1:13
.= (iter (f,(l + n))) . z by FUNCT_7:77 ;
hence  S1[x,z] by A4, A5; ::_thesis: verum
end;
A12: for x, y being set st S1[x,y] holds
S1[y,x] ;
consider EqR being Equivalence_Relation of E such that
A13: for x, y being set holds
( [x,y] in EqR iff ( x in E & y in E & S1[x,y] ) ) from EQREL_1:sch_1(A1, A12, A3);
take  EqR ; ::_thesis: for x, y being set st x in E & y in E holds
( [x,y] in EqR iff ex k, l being Element of NAT st (iter (f,k)) . x = (iter (f,l)) . y )
let x, y be set ; ::_thesis: ( x in E & y in E implies ( [x,y] in EqR iff ex k, l being Element of NAT st (iter (f,k)) . x = (iter (f,l)) . y ) )
assume  ( x in E & y in E ) ; ::_thesis: ( [x,y] in EqR iff ex k, l being Element of NAT st (iter (f,k)) . x = (iter (f,l)) . y )
hence  ( [x,y] in EqR iff ex k, l being Element of NAT st (iter (f,k)) . x = (iter (f,l)) . y ) by A13; ::_thesis: verum
end;
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 Element of 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 Element of NAT st (iter (f,k)) . x = (iter (f,l)) . y ) ) holds
b1 = b2
proof
let IT1, IT2 be Equivalence_Relation of E; ::_thesis: ( ( for x, y being set st x in E & y in E holds
( [x,y] in IT1 iff ex k, l being Element of 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 IT2 iff ex k, l being Element of NAT st (iter (f,k)) . x = (iter (f,l)) . y ) ) implies IT1 = IT2 )
assume that
A14: for x, y being set st x in E & y in E holds
( [x,y] in IT1 iff ex k, l being Element of NAT st (iter (f,k)) . x = (iter (f,l)) . y ) and
A15: for x, y being set st x in E & y in E holds
( [x,y] in IT2 iff ex k, l being Element of NAT st (iter (f,k)) . x = (iter (f,l)) . y ) ; ::_thesis: IT1 = IT2
let a, b be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [a,b] in IT1 or [a,b] in IT2 ) & ( not [a,b] in IT2 or [a,b] in IT1 ) )
hereby  ::_thesis: ( not [a,b] in IT2 or [a,b] in IT1 )
assume A16: [a,b] in IT1 ; ::_thesis: [a,b] in IT2
then A17: ( a in E & b in E ) by ZFMISC_1:87;
then  ex k, l being Element of NAT st (iter (f,k)) . a = (iter (f,l)) . b by A14, A16;
hence  [a,b] in IT2 by A15, A17; ::_thesis: verum
end;
assume A18: [a,b] in IT2 ; ::_thesis: [a,b] in IT1
then A19: ( a in E & b in E ) by ZFMISC_1:87;
then  ex k, l being Element of NAT st (iter (f,k)) . a = (iter (f,l)) . b by A15, A18;
hence  [a,b] in IT1 by A14, A19; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines =_ ABIAN:def_7_:_
 for E being set
for f being Function of E,E
for b3 being Equivalence_Relation of E holds
( b3 = =_ f iff for x, y being set st x in E & y in E holds
( [x,y] in b3 iff ex k, l being Element of NAT st (iter (f,k)) . x = (iter (f,l)) . y ) );

theorem Th6: :: ABIAN:6
for E being non empty set
for f being Function of E,E
for c being Element of Class (=_ f)
for e being Element of c holds f . e in c
proof
let E be non empty set ; ::_thesis: for f being Function of E,E
for c being Element of Class (=_ f)
for e being Element of c holds f . e in c
let f be Function of E,E; ::_thesis: for c being Element of Class (=_ f)
for e being Element of c holds f . e in c
let c be Element of Class (=_ f); ::_thesis: for e being Element of c holds f . e in c
let e be Element of c; ::_thesis: f . e in c
 dom f = E by FUNCT_2:def_1;
then A1: f . e in (dom f) \/ (rng f) by XBOOLE_0:def_3;
 ex x9 being set st
( x9 in E & c = Class ((=_ f),x9) ) by EQREL_1:def_3;
then A2: c = Class ((=_ f),e) by EQREL_1:23;
(iter (f,1)) . e = f . e by FUNCT_7:70
.= (id (field f)) . (f . e) by A1, FUNCT_1:17
.= (iter (f,0)) . (f . e) by FUNCT_7:68 ;
then  [(f . e),e] in =_ f by Def7;
hence  f . e in c by A2, EQREL_1:19; ::_thesis: verum
end;

theorem Th7: :: ABIAN:7
for E being non empty set
for f being Function of E,E
for c being Element of Class (=_ f)
for e being Element of c
for n being Element of NAT holds (iter (f,n)) . e in c
proof
let E be non empty set ; ::_thesis: for f being Function of E,E
for c being Element of Class (=_ f)
for e being Element of c
for n being Element of NAT holds (iter (f,n)) . e in c
let f be Function of E,E; ::_thesis: for c being Element of Class (=_ f)
for e being Element of c
for n being Element of NAT holds (iter (f,n)) . e in c
let c be Element of Class (=_ f); ::_thesis: for e being Element of c
for n being Element of NAT holds (iter (f,n)) . e in c
let e be Element of c; ::_thesis: for n being Element of NAT holds (iter (f,n)) . e in c
let n be Element of NAT ; ::_thesis: (iter (f,n)) . e in c
 dom f = E by FUNCT_2:def_1;
then  (iter (f,n)) . e in (dom f) \/ (rng f) by XBOOLE_0:def_3;
then (iter (f,n)) . e = (id (field f)) . ((iter (f,n)) . e) by FUNCT_1:17
.= (iter (f,0)) . ((iter (f,n)) . e) by FUNCT_7:68 ;
then A1: [((iter (f,n)) . e),e] in =_ f by Def7;
 ex x9 being set st
( x9 in E & c = Class ((=_ f),x9) ) by EQREL_1:def_3;
then  c = Class ((=_ f),e) by EQREL_1:23;
hence  (iter (f,n)) . e in c by A1, EQREL_1:19; ::_thesis: verum
end;

registration
cluster empty-membered  ->  trivial for set ;
coherence
 for b1 being set st b1 is empty-membered holds
b1 is trivial ;
end;

registration
let A be set ;
let B be with_non-empty_element set ;
cluster Relation-like non-empty A -defined B -valued Function-like V33(A,B) for Element of bool [:A,B:];
existence
 ex b1 being Function of A,B st b1 is non-empty
proof
consider X being non empty set  such that
A1: X in B by SETFAM_1:def_10;
reconsider f = A --> X as Function of A,B by A1, FUNCOP_1:45;
take  f ; ::_thesis: f is non-empty
let n be set ; :: according to FUNCT_1:def_9 ::_thesis: ( not n in dom f or not f . n is empty )
assume  n in dom f ; ::_thesis: not f . n is empty
then  n in A by FUNCOP_1:13;
hence  not f . n is empty by FUNCOP_1:7; ::_thesis: verum
end;
end;

registration
let A be non empty set ;
let B be with_non-empty_element set ;
let f be non-empty Function of A,B;
let a be Element of A;
clusterf . a ->  non empty ;
coherence
 not f . a is empty
proof
 dom f = A by FUNCT_2:def_1;
then  f . a in rng f by FUNCT_1:def_3;
hence  not f . a is empty ; ::_thesis: verum
end;
end;

registration
let X be non empty set ;
cluster bool X ->  with_non-empty_element ;
coherence
 not bool X is empty-membered
proof
take  X ; :: according to SETFAM_1:def_10 ::_thesis: X in bool X
thus  X in bool X by ZFMISC_1:def_1; ::_thesis: verum
end;
end;

theorem :: ABIAN:8
for E being non empty set
for f being Function of E,E st f is without_fixpoints holds
ex E1, E2, E3 being set st
( (E1 \/ E2) \/ E3 = E & f .: E1 misses E1 & f .: E2 misses E2 & f .: E3 misses E3 )
proof
let E be non empty set ; ::_thesis: for f being Function of E,E st f is without_fixpoints holds
ex E1, E2, E3 being set st
( (E1 \/ E2) \/ E3 = E & f .: E1 misses E1 & f .: E2 misses E2 & f .: E3 misses E3 )
let f be Function of E,E; ::_thesis: ( f is without_fixpoints implies ex E1, E2, E3 being set st
( (E1 \/ E2) \/ E3 = E & f .: E1 misses E1 & f .: E2 misses E2 & f .: E3 misses E3 ) )
defpred S1[ set , Element of [:(bool E),(bool E),(bool E):]] means ( (($2 `1_3) \/ ($2 `2_3)) \/ ($2 `3_3) = $1 & f .: ($2 `1_3) misses $2 `1_3 & f .: ($2 `2_3) misses $2 `2_3 & f .: ($2 `3_3) misses $2 `3_3 );
deffunc H1( Element of NAT ) ->  Function of E,E = iter (f,$1);
assume A1: f is without_fixpoints ; ::_thesis: ex E1, E2, E3 being set st
( (E1 \/ E2) \/ E3 = E & f .: E1 misses E1 & f .: E2 misses E2 & f .: E3 misses E3 )
A2: for a being Element of Class (=_ f) ex b being Element of [:(bool E),(bool E),(bool E):] st S1[a,b]
proof
reconsider c3 = {} as Subset of E by XBOOLE_1:2;
let c be Element of Class (=_ f); ::_thesis: ex b being Element of [:(bool E),(bool E),(bool E):] st S1[c,b]
consider x0 being set  such that
A3: x0 in E and
A4: c = Class ((=_ f),x0) by EQREL_1:def_3;
reconsider x0 = x0 as Element of c by A3, A4, EQREL_1:20;
defpred S2[ set ] means  ex k, l being Element of NAT st
( H1(k) . $1 = H1(l) . x0 & k is even & l is even );
set c1 =  {  x where x is Element of c : S2[x]  }  ;
  {  x where x is Element of c : S2[x]  }  is Subset of c from DOMAIN_1:sch_7();
then reconsider c1 =  {  x where x is Element of c : S2[x]  }  as Subset of E by XBOOLE_1:1;
defpred S3[ set ] means  ex k, l being Element of NAT st
( H1(k) . $1 = H1(l) . x0 & k is odd & l is even );
set c2 =  {  x where x is Element of c : S3[x]  }  ;
  {  x where x is Element of c : S3[x]  }  is Subset of c from DOMAIN_1:sch_7();
then reconsider c2 =  {  x where x is Element of c : S3[x]  }  as Subset of E by XBOOLE_1:1;
percases ( c1 misses c2 or c1 meets c2 ) ;
supposeA5: c1 misses c2 ; ::_thesis: ex b being Element of [:(bool E),(bool E),(bool E):] st S1[c,b]
take b = [c1,c2,c3]; ::_thesis: S1[c,b]
A6: b `2_3 = c2 by MCART_1:def_6;
A7: b `3_3 = c3 by MCART_1:def_7;
A8: b `1_3 = c1 by MCART_1:def_5;
thus  ((b `1_3) \/ (b `2_3)) \/ (b `3_3) = c ::_thesis: ( f .: (b `1_3) misses b `1_3 & f .: (b `2_3) misses b `2_3 & f .: (b `3_3) misses b `3_3 )
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: c c= ((b `1_3) \/ (b `2_3)) \/ (b `3_3)
let x be set ; ::_thesis: ( x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3) implies b1 in c )
assume A9: x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3) ; ::_thesis: b1 in c
percases ( x in c1 or x in c2 or x in c3 ) by A8, A6, A7, A9, XBOOLE_0:def_3;
suppose x in c1 ; ::_thesis: b1 in c
then  ex xx being Element of c st
( x = xx & ex k, l being Element of NAT st
( H1(k) . xx = H1(l) . x0 & k is even & l is even ) ) ;
hence  x in c ; ::_thesis: verum
end;
suppose x in c2 ; ::_thesis: b1 in c
then  ex xx being Element of c st
( x = xx & ex k, l being Element of NAT st
( H1(k) . xx = H1(l) . x0 & k is odd & l is even ) ) ;
hence  x in c ; ::_thesis: verum
end;
suppose x in c3 ; ::_thesis: b1 in c
hence  x in c ; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in c or x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3) )
assume  x in c ; ::_thesis: x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3)
then reconsider xc = x as Element of c ;
 [xc,x0] in =_ f by A4, EQREL_1:19;
then consider k, l being Element of NAT  such that
A10: H1(k) . xc = H1(l) . x0 by Def7;
A11: dom H1(l) = E by FUNCT_2:def_1;
A12: dom H1(k) = E by FUNCT_2:def_1;
percases ( k is even or k is odd ) ;
supposeA13: k is even ; ::_thesis: x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3)
then reconsider k = k as even Element of NAT ;
thus  x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3) ::_thesis: verum
proof
percases ( l is even or l is odd ) ;
suppose l is even ; ::_thesis: x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3)
then  xc in c1 by A10, A13;
hence  x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3) by A8, A7, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose l is odd ; ::_thesis: x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3)
then reconsider l = l as odd Element of NAT ;
H1(k + 1) . xc = (f * H1(k)) . xc by FUNCT_7:71
.= f . (H1(l) . x0) by A10, A12, FUNCT_1:13
.= (f * H1(l)) . x0 by A11, FUNCT_1:13
.= H1(l + 1) . x0 by FUNCT_7:71 ;
then  xc in c2 ;
hence  x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3) by A6, A7, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
end;
supposeA14: k is odd ; ::_thesis: x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3)
then reconsider k = k as odd Element of NAT ;
thus  x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3) ::_thesis: verum
proof
percases ( l is even or l is odd ) ;
suppose l is even ; ::_thesis: x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3)
then  xc in c2 by A10, A14;
hence  x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3) by A6, A7, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose l is odd ; ::_thesis: x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3)
then reconsider l = l as odd Element of NAT ;
H1(k + 1) . xc = (f * H1(k)) . xc by FUNCT_7:71
.= f . (H1(l) . x0) by A10, A12, FUNCT_1:13
.= (f * H1(l)) . x0 by A11, FUNCT_1:13
.= H1(l + 1) . x0 by FUNCT_7:71 ;
then  xc in c1 ;
hence  x in ((b `1_3) \/ (b `2_3)) \/ (b `3_3) by A8, A7, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
end;
end;
end;
 f .: c1 c= c2
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: c1 or y in c2 )
A15: dom f = E by FUNCT_2:def_1;
assume  y in f .: c1 ; ::_thesis: y in c2
then consider x being set  such that
 x in dom f and
A16: x in c1 and
A17: y = f . x by FUNCT_1:def_6;
consider xx being Element of c such that
A18: x = xx and
A19: ex k, l being Element of NAT st
( H1(k) . xx = H1(l) . x0 & k is even & l is even ) by A16;
consider k, l being Element of NAT  such that
A20: H1(k) . xx = H1(l) . x0 and
A21: ( k is even & l is even ) by A19;
reconsider k = k, l = l as even Element of NAT by A21;
reconsider k1 = k + 1 as odd Element of NAT ;
reconsider l1 = l + 1 as odd Element of NAT ;
reconsider l2 = l1 + 1 as even Element of NAT ;
A22: dom H1(k) = E by FUNCT_2:def_1;
reconsider yc = y as Element of c by A17, A18, Th6;
A23: dom H1(l) = E by FUNCT_2:def_1;
A24: dom H1(k1) = E by FUNCT_2:def_1;
A25: H1(k1 + 1) . xx = (H1(k1) * f) . xx by FUNCT_7:69
.= H1(k1) . (f . xx) by A15, FUNCT_1:13 ;
A26: dom H1(l1) = E by FUNCT_2:def_1;
H1(k1 + 1) . xx = (f * H1(k1)) . xx by FUNCT_7:71
.= f . (H1(k1) . xx) by A24, FUNCT_1:13
.= f . ((f * H1(k)) . xx) by FUNCT_7:71
.= f . (f . (H1(l) . x0)) by A20, A22, FUNCT_1:13
.= f . ((f * H1(l)) . x0) by A23, FUNCT_1:13
.= f . (H1(l1) . x0) by FUNCT_7:71
.= (f * H1(l1)) . x0 by A26, FUNCT_1:13
.= H1(l2) . x0 by FUNCT_7:71 ;
then  yc in c2 by A17, A18, A25;
hence  y in c2 ; ::_thesis: verum
end;
hence  f .: (b `1_3) misses b `1_3 by A5, A8, XBOOLE_1:63; ::_thesis: ( f .: (b `2_3) misses b `2_3 & f .: (b `3_3) misses b `3_3 )
 f .: c2 c= c1
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: c2 or y in c1 )
A27: dom f = E by FUNCT_2:def_1;
assume  y in f .: c2 ; ::_thesis: y in c1
then consider x being set  such that
 x in dom f and
A28: x in c2 and
A29: y = f . x by FUNCT_1:def_6;
consider xx being Element of c such that
A30: x = xx and
A31: ex k, l being Element of NAT st
( H1(k) . xx = H1(l) . x0 & k is odd & l is even ) by A28;
consider k, l being Element of NAT  such that
A32: H1(k) . xx = H1(l) . x0 and
A33: k is odd and
A34: l is even by A31;
reconsider l = l as even Element of NAT by A34;
reconsider k = k as odd Element of NAT by A33;
reconsider k1 = k + 1 as even Element of NAT ;
reconsider l1 = l + 1 as odd Element of NAT ;
reconsider l2 = l1 + 1 as even Element of NAT ;
A35: dom H1(k) = E by FUNCT_2:def_1;
reconsider yc = y as Element of c by A29, A30, Th6;
A36: dom H1(l) = E by FUNCT_2:def_1;
A37: dom H1(k1) = E by FUNCT_2:def_1;
A38: H1(k1 + 1) . xx = (H1(k1) * f) . xx by FUNCT_7:69
.= H1(k1) . (f . xx) by A27, FUNCT_1:13 ;
A39: dom H1(l1) = E by FUNCT_2:def_1;
H1(k1 + 1) . xx = (f * H1(k1)) . xx by FUNCT_7:71
.= f . (H1(k1) . xx) by A37, FUNCT_1:13
.= f . ((f * H1(k)) . xx) by FUNCT_7:71
.= f . (f . (H1(l) . x0)) by A32, A35, FUNCT_1:13
.= f . ((f * H1(l)) . x0) by A36, FUNCT_1:13
.= f . (H1(l1) . x0) by FUNCT_7:71
.= (f * H1(l1)) . x0 by A39, FUNCT_1:13
.= H1(l2) . x0 by FUNCT_7:71 ;
then  yc in c1 by A29, A30, A38;
hence  y in c1 ; ::_thesis: verum
end;
hence  f .: (b `2_3) misses b `2_3 by A5, A6, XBOOLE_1:63; ::_thesis: f .: (b `3_3) misses b `3_3
thus  f .: (b `3_3) misses b `3_3 by A7, XBOOLE_1:65; ::_thesis: verum
end;
suppose c1 meets c2 ; ::_thesis: ex b being Element of [:(bool E),(bool E),(bool E):] st S1[c,b]
then consider x1 being set  such that
A40: x1 in c1 and
A41: x1 in c2 by XBOOLE_0:3;
consider x11 being Element of c such that
A42: x1 = x11 and
A43: ex k, l being Element of NAT st
( H1(k) . x11 = H1(l) . x0 & k is even & l is even ) by A40;
consider x12 being Element of c such that
A44: x1 = x12 and
A45: ex k, l being Element of NAT st
( H1(k) . x12 = H1(l) . x0 & k is odd & l is even ) by A41;
consider k2, l2 being Element of NAT  such that
A46: H1(k2) . x12 = H1(l2) . x0 and
A47: k2 is odd and
A48: l2 is even by A45;
reconsider x1 = x1 as Element of c by A42;
consider k1, l1 being Element of NAT  such that
A49: H1(k1) . x11 = H1(l1) . x0 and
A50: ( k1 is even & l1 is even ) by A43;
A51: dom H1(k1) = E by FUNCT_2:def_1;
A52: dom H1(l1) = E by FUNCT_2:def_1;
A53: H1(l2 + k1) . x1 = (H1(l2) * H1(k1)) . x1 by FUNCT_7:77
.= H1(l2) . (H1(l1) . x0) by A42, A49, A51, FUNCT_1:13
.= (H1(l2) * H1(l1)) . x0 by A52, FUNCT_1:13
.= H1(l1 + l2) . x0 by FUNCT_7:77 ;
A54: dom H1(l2) = E by FUNCT_2:def_1;
A55: dom H1(k2) = E by FUNCT_2:def_1;
A56: H1(l1 + k2) . x1 = (H1(l1) * H1(k2)) . x1 by FUNCT_7:77
.= H1(l1) . (H1(l2) . x0) by A44, A46, A55, FUNCT_1:13
.= (H1(l1) * H1(l2)) . x0 by A54, FUNCT_1:13
.= H1(l1 + l2) . x0 by FUNCT_7:77 ;
 ex r being Element of E ex k being odd Element of NAT st
( H1(k) . r = r & r in c )
proof
reconsider k2 = k2 as odd Element of NAT by A47;
reconsider k1 = k1, l1 = l1, l2 = l2 as even Element of NAT by A50, A48;
A57: dom H1(k1 + l2) = E by FUNCT_2:def_1;
A58: dom H1(k2 + l1) = E by FUNCT_2:def_1;
percases ( k1 + l2 < k2 + l1 or k1 + l2 > k2 + l1 ) by XXREAL_0:1;
suppose k1 + l2 < k2 + l1 ; ::_thesis: ex r being Element of E ex k being odd Element of NAT st
( H1(k) . r = r & r in c )
then reconsider k = (k2 + l1) - (k1 + l2) as Element of NAT by INT_1:5;
take r = H1(k1 + l2) . x1; ::_thesis: ex k being odd Element of NAT st
( H1(k) . r = r & r in c )
reconsider k = k as odd Element of NAT ;
take  k ; ::_thesis: ( H1(k) . r = r & r in c )
H1(k) . (H1(k1 + l2) . x1) = (H1(k) * H1(k1 + l2)) . x1 by A57, FUNCT_1:13
.= H1(k + (k1 + l2)) . x1 by FUNCT_7:77
.= H1(k1 + l2) . x1 by A56, A53 ;
hence  H1(k) . r = r ; ::_thesis: r in c
thus  r in c by Th7; ::_thesis: verum
end;
suppose k1 + l2 > k2 + l1 ; ::_thesis: ex r being Element of E ex k being odd Element of NAT st
( H1(k) . r = r & r in c )
then reconsider k = (k1 + l2) - (k2 + l1) as Element of NAT by INT_1:5;
take r = H1(k2 + l1) . x1; ::_thesis: ex k being odd Element of NAT st
( H1(k) . r = r & r in c )
reconsider k = k as odd Element of NAT ;
take  k ; ::_thesis: ( H1(k) . r = r & r in c )
H1(k) . (H1(k2 + l1) . x1) = (H1(k) * H1(k2 + l1)) . x1 by A58, FUNCT_1:13
.= H1(k + (k2 + l1)) . x1 by FUNCT_7:77
.= H1(k2 + l1) . x1 by A56, A53 ;
hence  H1(k) . r = r ; ::_thesis: r in c
thus  r in c by Th7; ::_thesis: verum
end;
end;
end;
then consider r being Element of E, k being odd Element of NAT  such that
A59: H1(k) . r = r and
A60: r in c ;
reconsider r = r as Element of c by A60;
deffunc H2( set ) ->  set =  {  l where l is Element of NAT : H1(l) . $1 = r  }  ;
A61: for x being Element of c holds H2(x) in bool NAT
proof
let x be Element of c; ::_thesis: H2(x) in bool NAT
defpred S4[ Element of NAT ] means H1($1) . x = r;
  {  l where l is Element of NAT : S4[l]  }  is Subset of NAT from DOMAIN_1:sch_7();
hence  H2(x) in bool NAT ; ::_thesis: verum
end;
consider Odl being Function of c,(bool NAT) such that
A62: for x being Element of c holds Odl . x = H2(x) from FUNCT_2:sch_8(A61);
now__::_thesis:_for_n_being_set_st_n_in_dom_Odl_holds_
not_Odl_._n_is_empty
defpred S4[ Element of NAT ] means H1(k * $1) . r = r;
let n be set ; ::_thesis: ( n in dom Odl implies not Odl . n is empty )
assume  n in dom Odl ; ::_thesis: not Odl . n is empty
then reconsider nc = n as Element of c by FUNCT_2:def_1;
A63: Odl . nc =  {  l where l is Element of NAT : H1(l) . nc = r  }  by A62;
A64: now__::_thesis:_for_i_being_Element_of_NAT_st_S4[i]_holds_
S4[i_+_1]
let i be Element of NAT ; ::_thesis: ( S4[i] implies S4[i + 1] )
assume A65: S4[i] ; ::_thesis: S4[i + 1]
A66: dom H1(k) = E by FUNCT_2:def_1;
H1(k * (i + 1)) . r = H1((k * i) + (k * 1)) . r
.= (H1(k * i) * H1(k)) . r by FUNCT_7:77
.= r by A59, A65, A66, FUNCT_1:13 ;
hence  S4[i + 1] ; ::_thesis: verum
end;
A67: S4[ 0 ] by Th3;
A68: for i being Element of NAT holds S4[i] from NAT_1:sch_1(A67, A64);
 ex x9 being set st
( x9 in E & c = Class ((=_ f),x9) ) by EQREL_1:def_3;
then  [nc,r] in =_ f by EQREL_1:22;
then consider kn, ln being Element of NAT  such that
A69: (iter (f,kn)) . nc = (iter (f,ln)) . r by Def7;
A70: dom H1(ln) = E by FUNCT_2:def_1;
set mk = ln mod k;
set dk = ln div k;
A71: dom H1(kn) = E by FUNCT_2:def_1;
A72: 2 * 0 <> k ;
then  ln mod k < k by NAT_1:3, NAT_D:1;
then reconsider kmk = k - (ln mod k) as Element of NAT by INT_1:5;
 ln = (k * (ln div k)) + (ln mod k) by A72, NAT_1:3, NAT_D:2;
then A73: ln + kmk = k * ((ln div k) + 1) ;
H1(kmk + kn) . nc = (H1(kmk) * H1(kn)) . nc by FUNCT_7:77
.= H1(kmk) . (H1(ln) . r) by A69, A71, FUNCT_1:13
.= (H1(kmk) * H1(ln)) . r by A70, FUNCT_1:13
.= H1(k * ((ln div k) + 1)) . r by A73, FUNCT_7:77
.= r by A68 ;
then  kn + kmk in Odl . n by A63;
hence  not Odl . n is empty ; ::_thesis: verum
end;
then reconsider Odl = Odl as non-empty Function of c,(bool NAT) by FUNCT_1:def_9;
deffunc H3( Element of c) ->  Element of NAT = min (Odl . $1);
consider odl being Function of c,NAT such that
A74: for x being Element of c holds odl . x = H3(x) from FUNCT_2:sch_4();
defpred S4[ Element of c] means odl . $1 is even ;
set c1 =  {  x where x is Element of c : S4[x]  }  ;
set d1 =  {  x where x is Element of c : S4[x]  }  \ {r};
  {  x where x is Element of c : S4[x]  }  is Subset of c from DOMAIN_1:sch_7();
then A75:  {  x where x is Element of c : S4[x]  }  \ {r} c= c by XBOOLE_1:1;
 H1( 0 ) . r = r by Th3;
then  0 in  {  l where l is Element of NAT : H1(l) . r = r  }  ;
then  0 in Odl . r by A62;
then  min (Odl . r) = 0 by Th2;
then A76: odl . r = 2 * 0 by A74;
then A77: r in  {  x where x is Element of c : S4[x]  }  ;
reconsider d1 =  {  x where x is Element of c : S4[x]  }  \ {r} as Subset of E by A75, XBOOLE_1:1;
defpred S5[ Element of c] means odl . $1 is odd ;
set d2 =  {  x where x is Element of c : S5[x]  }  ;
  {  x where x is Element of c : S5[x]  }  is Subset of c from DOMAIN_1:sch_7();
then reconsider d2 =  {  x where x is Element of c : S5[x]  }  as Subset of E by XBOOLE_1:1;
A78: for x being Element of c st x <> r holds
odl . (f . x) = (odl . x) - 1
proof
let x be Element of c; ::_thesis: ( x <> r implies odl . (f . x) = (odl . x) - 1 )
reconsider fx = f . x as Element of c by Th6;
reconsider ofx = odl . fx, ox = odl . x as Element of NAT ;
assume A79: x <> r ; ::_thesis: odl . (f . x) = (odl . x) - 1
now__::_thesis:_not_odl_._x_=_0
assume  odl . x = 0 ; ::_thesis: contradiction
then  0 = min (Odl . x) by A74;
then  0 in Odl . x by XXREAL_2:def_7;
then  0 in  {  l where l is Element of NAT : H1(l) . x = r  }  by A62;
then  ex l being Element of NAT st
( l = 0 & H1(l) . x = r ) ;
hence  contradiction by A79, Th3; ::_thesis: verum
end;
then reconsider ox1 = ox - 1 as Element of NAT by INT_1:5, NAT_1:14;
 ox = min (Odl . x) by A74;
then  ox in Odl . x by XXREAL_2:def_7;
then  ox in  {  l where l is Element of NAT : H1(l) . x = r  }  by A62;
then A80: ex l being Element of NAT st
( l = ox & H1(l) . x = r ) ;
A81: dom f = E by FUNCT_2:def_1;
then H1(ox1) . fx = (H1(ox1) * f) . x by FUNCT_1:13
.= H1(ox1 + 1) . x by FUNCT_7:69
.= H1(ox) . x ;
then  ox1 in  {  l where l is Element of NAT : H1(l) . fx = r  }  by A80;
then A82: ox1 in Odl . fx by A62;
 ofx = min (Odl . fx) by A74;
then  ofx in Odl . fx by XXREAL_2:def_7;
then  ofx in  {  l where l is Element of NAT : H1(l) . fx = r  }  by A62;
then A83: ex l being Element of NAT st
( l = ofx & H1(l) . fx = r ) ;
H1(ofx + 1) . x = (H1(ofx) * f) . x by FUNCT_7:69
.= H1(ofx) . fx by A81, FUNCT_1:13 ;
then  ofx + 1 in  {  l where l is Element of NAT : H1(l) . x = r  }  by A83;
then A84: ofx + 1 in Odl . x by A62;
 ox = min (Odl . x) by A74;
then  ofx + 1 >= ox by A84, XXREAL_2:def_7;
then A85: ofx >= ox - 1 by XREAL_1:20;
 ofx = min (Odl . fx) by A74;
then  ofx <= ox - 1 by A82, XXREAL_2:def_7;
hence  odl . (f . x) = (odl . x) - 1 by A85, XXREAL_0:1; ::_thesis: verum
end;
A86: f .: d1 c= d2
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: d1 or y in d2 )
assume  y in f .: d1 ; ::_thesis: y in d2
then consider x being set  such that
 x in dom f and
A87: x in d1 and
A88: y = f . x by FUNCT_1:def_6;
 x in  {  x where x is Element of c : S4[x]  }  by A87;
then consider xx being Element of c such that
A89: x = xx and
A90: odl . xx is even ;
reconsider ox = odl . xx as even Element of NAT by A90;
reconsider yc = y as Element of c by A88, A89, Th6;
 r <> xx by A87, A89, ZFMISC_1:56;
then  odl . yc = ox - 1 by A78, A88, A89;
hence  y in d2 ; ::_thesis: verum
end;
A91:  {  x where x is Element of c : S4[x]  }  \/ d2 = c
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: c c=  {  x where x is Element of c : S4[x]  }  \/ d2
let x be set ; ::_thesis: ( x in  {  x where x is Element of c : S4[x]  }  \/ d2 implies b1 in c )
assume A92: x in  {  x where x is Element of c : S4[x]  }  \/ d2 ; ::_thesis: b1 in c
percases ( x in  {  x where x is Element of c : S4[x]  }  or x in d2 ) by A92, XBOOLE_0:def_3;
suppose x in  {  x where x is Element of c : S4[x]  }  ; ::_thesis: b1 in c
then  ex xc being Element of c st
( xc = x & odl . xc is even ) ;
hence  x in c ; ::_thesis: verum
end;
suppose x in d2 ; ::_thesis: b1 in c
then  ex xc being Element of c st
( xc = x & odl . xc is odd ) ;
hence  x in c ; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in c or x in  {  x where x is Element of c : S4[x]  }  \/ d2 )
assume  x in c ; ::_thesis: x in  {  x where x is Element of c : S4[x]  }  \/ d2
then reconsider xc = x as Element of c ;
 ( odl . xc is even or odl . xc is odd ) ;
then  ( x in  {  x where x is Element of c : S4[x]  }  or x in d2 ) ;
hence  x in  {  x where x is Element of c : S4[x]  }  \/ d2 by XBOOLE_0:def_3; ::_thesis: verum
end;
reconsider d3 = {r} as Subset of E by ZFMISC_1:31;
take b = [d1,d2,d3]; ::_thesis: S1[c,b]
A93: b `1_3 = d1 by MCART_1:def_5;
A94: b `2_3 = d2 by MCART_1:def_6;
A95: b `3_3 = d3 by MCART_1:def_7;
d1 \/ d3 =  {  x where x is Element of c : S4[x]  }  \/ d3 by XBOOLE_1:39
.=  {  x where x is Element of c : S4[x]  }  by A77, ZFMISC_1:40 ;
hence  ((b `1_3) \/ (b `2_3)) \/ (b `3_3) = c by A93, A94, A95, A91, XBOOLE_1:4; ::_thesis: ( f .: (b `1_3) misses b `1_3 & f .: (b `2_3) misses b `2_3 & f .: (b `3_3) misses b `3_3 )
A96:  {  x where x is Element of c : S4[x]  }  misses d2
proof
assume   {  x where x is Element of c : S4[x]  }  meets d2 ; ::_thesis: contradiction
then consider z being set  such that
A97: ( z in  {  x where x is Element of c : S4[x]  }  & z in d2 ) by XBOOLE_0:3;
 ( ex x being Element of c st
( z = x & odl . x is even ) & ex x being Element of c st
( z = x & odl . x is odd ) ) by A97;
hence  contradiction ; ::_thesis: verum
end;
then  d1 misses d2 by XBOOLE_1:63;
hence  f .: (b `1_3) misses b `1_3 by A93, A86, XBOOLE_1:63; ::_thesis: ( f .: (b `2_3) misses b `2_3 & f .: (b `3_3) misses b `3_3 )
 f .: d2 c=  {  x where x is Element of c : S4[x]  }
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: d2 or y in  {  x where x is Element of c : S4[x]  }  )
assume  y in f .: d2 ; ::_thesis: y in  {  x where x is Element of c : S4[x]  }
then consider x being set  such that
 x in dom f and
A98: x in d2 and
A99: y = f . x by FUNCT_1:def_6;
consider xx being Element of c such that
A100: x = xx and
A101: odl . xx is odd by A98;
reconsider ox = odl . xx as odd Element of NAT by A101;
reconsider yc = y as Element of c by A99, A100, Th6;
 odl . yc = ox - 1 by A76, A78, A99, A100;
hence  y in  {  x where x is Element of c : S4[x]  }  ; ::_thesis: verum
end;
hence  f .: (b `2_3) misses b `2_3 by A94, A96, XBOOLE_1:63; ::_thesis: f .: (b `3_3) misses b `3_3
thus  f .: (b `3_3) misses b `3_3 ::_thesis: verum
proof
assume  f .: (b `3_3) meets b `3_3 ; ::_thesis: contradiction
then consider y being set  such that
A102: y in f .: (b `3_3) and
A103: y in b `3_3 by XBOOLE_0:3;
A104: y = r by A95, A103, TARSKI:def_1;
consider x being set  such that
 x in dom f and
A105: x in {r} and
A106: y = f . x by A95, A102, FUNCT_1:def_6;
 x = r by A105, TARSKI:def_1;
then  r is_a_fixpoint_of f by A104, A106, Def4;
hence  contradiction by A1, Def5; ::_thesis: verum
end;
end;
end;
end;
consider F being Function of (Class (=_ f)),[:(bool E),(bool E),(bool E):] such that
A107: for a being Element of Class (=_ f) holds S1[a,F . a] from FUNCT_2:sch_3(A2);
set E3c =  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  ;
set E2c =  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  ;
set E1c =  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ;
set E1 = union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ;
set E2 = union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  ;
set E3 = union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  ;
take  union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ; ::_thesis: ex E2, E3 being set st
( ((union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ) \/ E2) \/ E3 = E & f .: (union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ) misses union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  & f .: E2 misses E2 & f .: E3 misses E3 )
take  union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  ; ::_thesis: ex E3 being set st
( ((union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ) \/ (union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  )) \/ E3 = E & f .: (union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ) misses union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  & f .: (union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  ) misses union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  & f .: E3 misses E3 )
take  union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  ; ::_thesis: ( ((union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ) \/ (union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  )) \/ (union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  ) = E & f .: (union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ) misses union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  & f .: (union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  ) misses union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  & f .: (union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  ) misses union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  )
thus  ((union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ) \/ (union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  )) \/ (union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  ) = E ::_thesis: ( f .: (union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ) misses union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  & f .: (union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  ) misses union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  & f .: (union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  ) misses union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  )
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: E c= ((union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ) \/ (union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  )) \/ (union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  )
let x be set ; ::_thesis: ( x in ((union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ) \/ (union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  )) \/ (union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  ) implies b1 in E )
assume  x in ((union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ) \/ (union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  )) \/ (union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  ) ; ::_thesis: b1 in E
then A108: ( x in (union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ) \/ (union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  ) or x in union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  ) by XBOOLE_0:def_3;
percases ( x in union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  or x in union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  or x in union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  ) by A108, XBOOLE_0:def_3;
suppose x in union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ; ::_thesis: b1 in E
then consider Y being set  such that
A109: x in Y and
A110: Y in  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  by TARSKI:def_4;
 ex c being Element of Class (=_ f) st Y = (F . c) `1_3 by A110;
hence  x in E by A109; ::_thesis: verum
end;
suppose x in union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  ; ::_thesis: b1 in E
then consider Y being set  such that
A111: x in Y and
A112: Y in  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  by TARSKI:def_4;
 ex c being Element of Class (=_ f) st Y = (F . c) `2_3 by A112;
hence  x in E by A111; ::_thesis: verum
end;
suppose x in union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  ; ::_thesis: b1 in E
then consider Y being set  such that
A113: x in Y and
A114: Y in  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  by TARSKI:def_4;
 ex c being Element of Class (=_ f) st Y = (F . c) `3_3 by A114;
hence  x in E by A113; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in E or x in ((union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ) \/ (union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  )) \/ (union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  ) )
set c = Class ((=_ f),x);
assume A115: x in E ; ::_thesis: x in ((union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ) \/ (union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  )) \/ (union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  )
then A116: x in Class ((=_ f),x) by EQREL_1:20;
reconsider c = Class ((=_ f),x) as Element of Class (=_ f) by A115, EQREL_1:def_3;
 x in (((F . c) `1_3) \/ ((F . c) `2_3)) \/ ((F . c) `3_3) by A107, A116;
then A117: ( x in ((F . c) `1_3) \/ ((F . c) `2_3) or x in (F . c) `3_3 ) by XBOOLE_0:def_3;
percases ( x in (F . c) `1_3 or x in (F . c) `2_3 or x in (F . c) `3_3 ) by A117, XBOOLE_0:def_3;
supposeA118: x in (F . c) `1_3 ; ::_thesis: x in ((union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ) \/ (union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  )) \/ (union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  )
 (F . c) `1_3 in  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ;
then  x in union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  by A118, TARSKI:def_4;
then  x in (union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ) \/ (union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  ) by XBOOLE_0:def_3;
hence  x in ((union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ) \/ (union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  )) \/ (union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  ) by XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA119: x in (F . c) `2_3 ; ::_thesis: x in ((union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ) \/ (union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  )) \/ (union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  )
 (F . c) `2_3 in  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  ;
then  x in union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  by A119, TARSKI:def_4;
then  x in (union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ) \/ (union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  ) by XBOOLE_0:def_3;
hence  x in ((union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ) \/ (union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  )) \/ (union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  ) by XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA120: x in (F . c) `3_3 ; ::_thesis: x in ((union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ) \/ (union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  )) \/ (union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  )
 (F . c) `3_3 in  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  ;
then  x in union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  by A120, TARSKI:def_4;
hence  x in ((union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ) \/ (union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  )) \/ (union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  ) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
thus  f .: (union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ) misses union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ::_thesis: ( f .: (union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  ) misses union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  & f .: (union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  ) misses union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  )
proof
assume  not f .: (union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ) misses union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ; ::_thesis: contradiction
then consider x being set  such that
A121: x in f .: (union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  ) and
A122: x in union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  by XBOOLE_0:3;
consider Y being set  such that
A123: x in Y and
A124: Y in  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  by A122, TARSKI:def_4;
consider c being Element of Class (=_ f) such that
A125: Y = (F . c) `1_3 by A124;
 x in ((F . c) `1_3) \/ ((F . c) `2_3) by A123, A125, XBOOLE_0:def_3;
then  x in (((F . c) `1_3) \/ ((F . c) `2_3)) \/ ((F . c) `3_3) by XBOOLE_0:def_3;
then A126: x in c by A107;
 ex x9 being set st
( x9 in E & c = Class ((=_ f),x9) ) by EQREL_1:def_3;
then A127: c = Class ((=_ f),x) by A126, EQREL_1:23;
 dom f = E by FUNCT_2:def_1;
then A128: x in (dom f) \/ (rng f) by A123, A125, XBOOLE_0:def_3;
consider xx being set  such that
A129: xx in dom f and
A130: xx in union  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  and
A131: x = f . xx by A121, FUNCT_1:def_6;
consider YY being set  such that
A132: xx in YY and
A133: YY in  {  ((F . c) `1_3) where c is Element of Class (=_ f) : verum  }  by A130, TARSKI:def_4;
consider cc being Element of Class (=_ f) such that
A134: YY = (F . cc) `1_3 by A133;
 xx in ((F . cc) `1_3) \/ ((F . cc) `2_3) by A132, A134, XBOOLE_0:def_3;
then  xx in (((F . cc) `1_3) \/ ((F . cc) `2_3)) \/ ((F . cc) `3_3) by XBOOLE_0:def_3;
then A135: xx in cc by A107;
 ex xx9 being set st
( xx9 in E & cc = Class ((=_ f),xx9) ) by EQREL_1:def_3;
then A136: cc = Class ((=_ f),xx) by A135, EQREL_1:23;
(iter (f,1)) . xx = x by A131, FUNCT_7:70
.= (id (field f)) . x by A128, FUNCT_1:17
.= (iter (f,0)) . x by FUNCT_7:68 ;
then  [x,xx] in =_ f by A123, A125, A132, A134, Def7;
then A137: Class ((=_ f),x) = Class ((=_ f),xx) by A123, A125, EQREL_1:35;
A138: f . xx in f .: YY by A129, A132, FUNCT_1:def_6;
 f .: YY misses YY by A107, A134;
hence  contradiction by A123, A125, A131, A134, A127, A136, A137, A138, XBOOLE_0:3; ::_thesis: verum
end;
thus  f .: (union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  ) misses union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  ::_thesis: f .: (union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  ) misses union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }
proof
assume  not f .: (union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  ) misses union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  ; ::_thesis: contradiction
then consider x being set  such that
A139: x in f .: (union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  ) and
A140: x in union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  by XBOOLE_0:3;
consider Y being set  such that
A141: x in Y and
A142: Y in  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  by A140, TARSKI:def_4;
consider c being Element of Class (=_ f) such that
A143: Y = (F . c) `2_3 by A142;
 x in ((F . c) `1_3) \/ ((F . c) `2_3) by A141, A143, XBOOLE_0:def_3;
then  x in (((F . c) `1_3) \/ ((F . c) `2_3)) \/ ((F . c) `3_3) by XBOOLE_0:def_3;
then A144: x in c by A107;
 ex x9 being set st
( x9 in E & c = Class ((=_ f),x9) ) by EQREL_1:def_3;
then A145: c = Class ((=_ f),x) by A144, EQREL_1:23;
 dom f = E by FUNCT_2:def_1;
then A146: x in (dom f) \/ (rng f) by A141, A143, XBOOLE_0:def_3;
consider xx being set  such that
A147: xx in dom f and
A148: xx in union  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  and
A149: x = f . xx by A139, FUNCT_1:def_6;
consider YY being set  such that
A150: xx in YY and
A151: YY in  {  ((F . c) `2_3) where c is Element of Class (=_ f) : verum  }  by A148, TARSKI:def_4;
consider cc being Element of Class (=_ f) such that
A152: YY = (F . cc) `2_3 by A151;
 xx in ((F . cc) `1_3) \/ ((F . cc) `2_3) by A150, A152, XBOOLE_0:def_3;
then  xx in (((F . cc) `1_3) \/ ((F . cc) `2_3)) \/ ((F . cc) `3_3) by XBOOLE_0:def_3;
then A153: xx in cc by A107;
 ex xx9 being set st
( xx9 in E & cc = Class ((=_ f),xx9) ) by EQREL_1:def_3;
then A154: cc = Class ((=_ f),xx) by A153, EQREL_1:23;
(iter (f,1)) . xx = x by A149, FUNCT_7:70
.= (id (field f)) . x by A146, FUNCT_1:17
.= (iter (f,0)) . x by FUNCT_7:68 ;
then  [x,xx] in =_ f by A141, A143, A150, A152, Def7;
then A155: Class ((=_ f),x) = Class ((=_ f),xx) by A141, A143, EQREL_1:35;
A156: f . xx in f .: YY by A147, A150, FUNCT_1:def_6;
 f .: YY misses YY by A107, A152;
hence  contradiction by A141, A143, A149, A152, A145, A154, A155, A156, XBOOLE_0:3; ::_thesis: verum
end;
thus  f .: (union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  ) misses union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  ::_thesis: verum
proof
assume  not f .: (union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  ) misses union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  ; ::_thesis: contradiction
then consider x being set  such that
A157: x in f .: (union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  ) and
A158: x in union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  by XBOOLE_0:3;
consider Y being set  such that
A159: x in Y and
A160: Y in  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  by A158, TARSKI:def_4;
consider c being Element of Class (=_ f) such that
A161: Y = (F . c) `3_3 by A160;
 x in (((F . c) `1_3) \/ ((F . c) `2_3)) \/ ((F . c) `3_3) by A159, A161, XBOOLE_0:def_3;
then A162: x in c by A107;
 ex x9 being set st
( x9 in E & c = Class ((=_ f),x9) ) by EQREL_1:def_3;
then A163: c = Class ((=_ f),x) by A162, EQREL_1:23;
 dom f = E by FUNCT_2:def_1;
then A164: x in (dom f) \/ (rng f) by A159, A161, XBOOLE_0:def_3;
consider xx being set  such that
A165: xx in dom f and
A166: xx in union  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  and
A167: x = f . xx by A157, FUNCT_1:def_6;
consider YY being set  such that
A168: xx in YY and
A169: YY in  {  ((F . c) `3_3) where c is Element of Class (=_ f) : verum  }  by A166, TARSKI:def_4;
consider cc being Element of Class (=_ f) such that
A170: YY = (F . cc) `3_3 by A169;
 xx in (((F . cc) `1_3) \/ ((F . cc) `2_3)) \/ ((F . cc) `3_3) by A168, A170, XBOOLE_0:def_3;
then A171: xx in cc by A107;
 ex xx9 being set st
( xx9 in E & cc = Class ((=_ f),xx9) ) by EQREL_1:def_3;
then A172: cc = Class ((=_ f),xx) by A171, EQREL_1:23;
(iter (f,1)) . xx = x by A167, FUNCT_7:70
.= (id (field f)) . x by A164, FUNCT_1:17
.= (iter (f,0)) . x by FUNCT_7:68 ;
then  [x,xx] in =_ f by A159, A161, A168, A170, Def7;
then A173: Class ((=_ f),x) = Class ((=_ f),xx) by A159, A161, EQREL_1:35;
A174: f . xx in f .: YY by A165, A168, FUNCT_1:def_6;
 f .: YY misses YY by A107, A170;
hence  contradiction by A159, A161, A167, A170, A163, A172, A173, A174, XBOOLE_0:3; ::_thesis: verum
end;
end;

begin

theorem :: ABIAN:9
for n being Nat holds
( n is odd iff ex k being Element of NAT st n = (2 * k) + 1 )
proof
let n be Nat; ::_thesis: ( n is odd iff ex k being Element of NAT st n = (2 * k) + 1 )
hereby  ::_thesis: ( ex k being Element of NAT st n = (2 * k) + 1 implies n is odd )
assume A1: n is odd ; ::_thesis: ex j being Element of NAT st n = (2 * j) + 1
then consider j being Integer such that
A2: n = (2 * j) + 1 by Th1;
now__::_thesis:_not_j_<_0
assume  j < 0 ; ::_thesis: contradiction
then A3: (2 * j) + 1 <= 2 * 0 by INT_1:7, XREAL_1:68;
percases ( (2 * j) + 1 < 0 or (2 * j) + 1 = 0 ) by A3;
suppose (2 * j) + 1 < 0 ; ::_thesis: contradiction
hence  contradiction by A2, NAT_1:2; ::_thesis: verum
end;
suppose (2 * j) + 1 = 0 ; ::_thesis: contradiction
then  n = 2 * 0 ;
hence  contradiction by A1; ::_thesis: verum
end;
end;
end;
then reconsider j = j as Element of NAT by INT_1:3;
take j = j; ::_thesis: n = (2 * j) + 1
thus  n = (2 * j) + 1 by A2; ::_thesis: verum
end;
thus  ( ex k being Element of NAT st n = (2 * k) + 1 implies n is odd ) ; ::_thesis: verum
end;

theorem :: ABIAN:10
for n being Element of NAT
for A being non empty set
for f being Function of A,A
for x being Element of A holds (iter (f,(n + 1))) . x = f . ((iter (f,n)) . x)
proof
let n be Element of NAT ; ::_thesis: for A being non empty set
for f being Function of A,A
for x being Element of A holds (iter (f,(n + 1))) . x = f . ((iter (f,n)) . x)
let A be non empty set ; ::_thesis: for f being Function of A,A
for x being Element of A holds (iter (f,(n + 1))) . x = f . ((iter (f,n)) . x)
let f be Function of A,A; ::_thesis: for x being Element of A holds (iter (f,(n + 1))) . x = f . ((iter (f,n)) . x)
let x be Element of A; ::_thesis: (iter (f,(n + 1))) . x = f . ((iter (f,n)) . x)
thus (iter (f,(n + 1))) . x = (f * (iter (f,n))) . x by FUNCT_7:71
.= f . ((iter (f,n)) . x) by FUNCT_2:15 ; ::_thesis: verum
end;

theorem :: ABIAN:11
for i being Integer holds
( i is even iff ex j being Integer st i = 2 * j ) by Lm1;

registration
cluster ext-real V10() V11() V12() V16() complex V18() integer odd for set ;
existence
 ex b1 being Nat st b1 is odd
proof
take  1 ; ::_thesis: 1 is odd
 1 = (2 * 0) + 1 ;
hence  1 is odd ; ::_thesis: verum
end;
cluster ext-real V10() V11() V12() V16() complex V18() integer even for set ;
existence
 ex b1 being Nat st b1 is even
proof
take  0 ; ::_thesis: 0 is even
 0 = 2 * 0 ;
hence  0 is even ; ::_thesis: verum
end;
end;

theorem Th12: :: ABIAN:12
for n being odd Nat holds 1 <= n
proof
let n be odd Nat; ::_thesis: 1 <= n
 2 * 0 < n by NAT_1:3;
then  0 + 1 <= n by NAT_1:13;
hence  1 <= n ; ::_thesis: verum
end;

registration
cluster integer odd  ->  non zero for set ;
coherence
 for b1 being Integer st b1 is odd holds
not b1 is zero by Th12;
end;