:: 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;