:: ABIAN semantic presentation

begin

definition
let i be ( ( integer ) ( ext-real complex V18() integer ) Integer) ;
attr i is even means :: ABIAN:def 1
2 : ( ( ) ( non empty ext-real positive non negative V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V74() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) divides i : ( ( ext-real ) ( ext-real ) set ) ;
end;

notation
let i be ( ( integer ) ( ext-real complex V18() integer ) Integer) ;
antonym odd i for even ;
end;

definition
let n be ( ( ) ( ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) ;
redefine attr n is even means :: ABIAN:def 2
 ex k being ( ( ) ( ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) st n : ( ( ext-real ) ( ext-real ) set ) = 2 : ( ( ) ( non empty ext-real positive non negative V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V74() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) * k : ( ( ) ( ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) ;
end;

registration
cluster ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() even for ( ( ) ( ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) ;
cluster ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() odd for ( ( ) ( ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) ;
cluster ext-real complex V18() integer even for ( ( ) ( ) set ) ;
cluster ext-real complex V18() integer odd for ( ( ) ( ) set ) ;
end;

theorem :: ABIAN:1
for i being ( ( integer ) ( ext-real complex V18() integer ) Integer) holds
( i : ( ( integer ) ( ext-real complex V18() integer ) Integer) is odd iff ex j being ( ( integer ) ( ext-real complex V18() integer ) Integer) st i : ( ( integer ) ( ext-real complex V18() integer ) Integer) = (2 : ( ( ) ( non empty ext-real positive non negative V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V74() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) * j : ( ( integer ) ( ext-real complex V18() integer ) Integer) ) : ( ( ) ( ext-real complex V18() integer ) set ) + 1 : ( ( ) ( non empty ext-real positive non negative V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V74() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real complex V18() integer ) set ) ) ;

registration
let i be ( ( integer ) ( ext-real complex V18() integer ) Integer) ;
cluster 2 : ( ( ) ( non empty ext-real positive non negative V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V74() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) * i : ( ( integer ) ( ext-real complex V18() integer ) set ) : ( ( ) ( ext-real complex V18() integer ) set ) -> even ;
end;

registration
let i be ( ( integer even ) ( ext-real complex V18() integer even ) Integer) ;
cluster i : ( ( integer even ) ( ext-real complex V18() integer even ) set ) + 1 : ( ( ) ( non empty ext-real positive non negative V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V74() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real complex V18() integer ) set ) -> odd ;
end;

registration
let i be ( ( integer odd ) ( ext-real complex V18() integer odd ) Integer) ;
cluster i : ( ( integer odd ) ( ext-real complex V18() integer odd ) set ) + 1 : ( ( ) ( non empty ext-real positive non negative V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V74() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real complex V18() integer ) set ) -> even ;
end;

registration
let i be ( ( integer even ) ( ext-real complex V18() integer even ) Integer) ;
cluster i : ( ( integer even ) ( ext-real complex V18() integer even ) set ) - 1 : ( ( ) ( non empty ext-real positive non negative V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V74() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real complex V18() integer ) set ) -> odd ;
end;

registration
let i be ( ( integer odd ) ( ext-real complex V18() integer odd ) Integer) ;
cluster i : ( ( integer odd ) ( ext-real complex V18() integer odd ) set ) - 1 : ( ( ) ( non empty ext-real positive non negative V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V74() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real complex V18() integer ) set ) -> even ;
end;

registration
let i be ( ( integer even ) ( ext-real complex V18() integer even ) Integer) ;
let j be ( ( integer ) ( ext-real complex V18() integer ) Integer) ;
cluster i : ( ( integer even ) ( ext-real complex V18() integer even ) set ) * j : ( ( integer ) ( ext-real complex V18() integer ) set ) : ( ( ) ( ext-real complex V18() integer ) set ) -> even ;
cluster j : ( ( integer ) ( ext-real complex V18() integer ) set ) * i : ( ( integer even ) ( ext-real complex V18() integer even ) set ) : ( ( ) ( ext-real complex V18() integer ) set ) -> even ;
end;

registration
let i, j be ( ( integer odd ) ( ext-real complex V18() integer odd ) Integer) ;
cluster i : ( ( integer odd ) ( ext-real complex V18() integer odd ) set ) * j : ( ( integer odd ) ( ext-real complex V18() integer odd ) set ) : ( ( ) ( ext-real complex V18() integer ) set ) -> odd ;
end;

registration
let i, j be ( ( integer even ) ( ext-real complex V18() integer even ) Integer) ;
cluster i : ( ( integer even ) ( ext-real complex V18() integer even ) set ) + j : ( ( integer even ) ( ext-real complex V18() integer even ) set ) : ( ( ) ( ext-real complex V18() integer ) set ) -> even ;
end;

registration
let i be ( ( integer even ) ( ext-real complex V18() integer even ) Integer) ;
let j be ( ( integer odd ) ( ext-real complex V18() integer odd ) Integer) ;
cluster i : ( ( integer even ) ( ext-real complex V18() integer even ) set ) + j : ( ( integer odd ) ( ext-real complex V18() integer odd ) set ) : ( ( ) ( ext-real complex V18() integer ) set ) -> odd ;
cluster j : ( ( integer odd ) ( ext-real complex V18() integer odd ) set ) + i : ( ( integer even ) ( ext-real complex V18() integer even ) set ) : ( ( ) ( ext-real complex V18() integer ) set ) -> odd ;
end;

registration
let i, j be ( ( integer odd ) ( ext-real complex V18() integer odd ) Integer) ;
cluster i : ( ( integer odd ) ( ext-real complex V18() integer odd ) set ) + j : ( ( integer odd ) ( ext-real complex V18() integer odd ) set ) : ( ( ) ( ext-real complex V18() integer ) set ) -> even ;
end;

registration
let i be ( ( integer even ) ( ext-real complex V18() integer even ) Integer) ;
let j be ( ( integer odd ) ( ext-real complex V18() integer odd ) Integer) ;
cluster i : ( ( integer even ) ( ext-real complex V18() integer even ) set ) - j : ( ( integer odd ) ( ext-real complex V18() integer odd ) set ) : ( ( ) ( ext-real complex V18() integer ) set ) -> odd ;
cluster j : ( ( integer odd ) ( ext-real complex V18() integer odd ) set ) - i : ( ( integer even ) ( ext-real complex V18() integer even ) set ) : ( ( ) ( ext-real complex V18() integer ) set ) -> odd ;
end;

registration
let i, j be ( ( integer odd ) ( ext-real complex V18() integer odd ) Integer) ;
cluster i : ( ( integer odd ) ( ext-real complex V18() integer odd ) set ) - j : ( ( integer odd ) ( ext-real complex V18() integer odd ) set ) : ( ( ) ( ext-real complex V18() integer ) set ) -> even ;
end;

registration
let m be ( ( integer even ) ( ext-real complex V18() integer even ) Integer) ;
cluster m : ( ( integer even ) ( ext-real complex V18() integer even ) set ) + 2 : ( ( ) ( non empty ext-real positive non negative V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V74() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real complex V18() integer ) set ) -> even ;
end;

registration
let m be ( ( integer odd ) ( ext-real complex V18() integer odd ) Integer) ;
cluster m : ( ( integer odd ) ( ext-real complex V18() integer odd ) set ) + 2 : ( ( ) ( non empty ext-real positive non negative V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V74() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real complex V18() integer ) set ) -> odd ;
end;

definition
let E be ( ( ) ( ) set ) ;
let f be ( ( Function-like V33(E : ( ( ) ( ) set ) ,E : ( ( ) ( ) set ) ) ) ( Relation-like E : ( ( ) ( ) set ) -defined E : ( ( ) ( ) set ) -valued Function-like V33(E : ( ( ) ( ) set ) ,E : ( ( ) ( ) set ) ) ) Function of E : ( ( ) ( ) set ) ,E : ( ( ) ( ) set ) ) ;
let n be ( ( ) ( ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) ;
:: original: iter
redefine func iter (f,n) -> ( ( Function-like V33(E : ( ( non empty ) ( non empty ) set ) ,E : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like E : ( ( non empty ) ( non empty ) set ) -defined E : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(E : ( ( non empty ) ( non empty ) set ) ,E : ( ( non empty ) ( non empty ) set ) ) ) Function of E : ( ( non empty ) ( non empty ) set ) ,E : ( ( non empty ) ( non empty ) set ) ) ;
end;

theorem :: ABIAN:2
for S being ( ( non empty ) ( non empty V58() V59() V60() V61() V62() V63() V74() V76() ) Subset of ( ( ) ( non empty ) set ) ) st 0 : ( ( ) ( empty ext-real non positive non negative V10() V11() V12() V14() V15() V16() complex V18() Function-like functional integer V57() V58() V59() V60() V61() V62() V63() V64() finite V69() V76() V77() V78() V79() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) in S : ( ( non empty ) ( non empty V58() V59() V60() V61() V62() V63() V74() V76() ) Subset of ( ( ) ( non empty ) set ) ) holds
min S : ( ( non empty ) ( non empty V58() V59() V60() V61() V62() V63() V74() V76() ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) = 0 : ( ( ) ( empty ext-real non positive non negative V10() V11() V12() V14() V15() V16() complex V18() Function-like functional integer V57() V58() V59() V60() V61() V62() V63() V64() finite V69() V76() V77() V78() V79() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: ABIAN:3
for E being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of E : ( ( non empty ) ( non empty ) set ) ,E : ( ( non empty ) ( non empty ) set ) )
for x being ( ( ) ( ) Element of E : ( ( non empty ) ( non empty ) set ) ) holds (iter (f : ( ( Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ,0 : ( ( ) ( empty ext-real non positive non negative V10() V11() V12() V14() V15() V16() complex V18() Function-like functional integer V57() V58() V59() V60() V61() V62() V63() V64() finite V69() V76() V77() V78() V79() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ;

definition
let x be ( ( ) ( ) set ) ;
let f be ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;
pred x is_a_fixpoint_of f means :: ABIAN:def 3
( x : ( ( non empty ) ( non empty ) set ) in dom f : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) & x : ( ( non empty ) ( non empty ) set ) = f : ( ( non empty ) ( non empty ) set ) . x : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) );
end;

definition
let A be ( ( non empty ) ( non empty ) set ) ;
let a be ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ;
let f be ( ( Function-like V33(A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like A : ( ( non empty ) ( non empty ) set ) -defined A : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) ) ) Function of A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) ) ;
:: original: is_a_fixpoint_of
redefine pred a is_a_fixpoint_of f means :: ABIAN:def 4
a : ( ( non empty ) ( non empty ) set ) = f : ( ( ) ( ) set ) . a : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ;
end;

definition
let f be ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;
attr f is with_fixpoint means :: ABIAN:def 5
 ex x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) is_a_fixpoint_of f : ( ( non empty ) ( non empty ) set ) ;
end;

notation
let f be ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;
antonym without_fixpoints f for with_fixpoint ;
end;

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

theorem :: ABIAN:4
for E being ( ( ) ( ) set )
for sE being ( ( ) ( ) Subset-Family of ) holds
( sE : ( ( ) ( ) Subset-Family of ) is covering iff union sE : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = E : ( ( ) ( ) set ) ) ;

registration
let E be ( ( ) ( ) set ) ;
cluster non empty finite covering for ( ( ) ( ) Element of bool (bool E : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: ABIAN:5
for E being ( ( ) ( ) set )
for f being ( ( Function-like V33(b1 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued Function-like V33(b1 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) ) ) Function of E : ( ( ) ( ) set ) ,E : ( ( ) ( ) set ) )
for sE being ( ( non empty covering ) ( non empty covering ) Subset-Family of ) st ( for X being ( ( ) ( ) Element of sE : ( ( non empty covering ) ( non empty covering ) Subset-Family of ) ) holds X : ( ( ) ( ) Element of b3 : ( ( non empty covering ) ( non empty covering ) Subset-Family of ) ) misses f : ( ( Function-like V33(b1 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued Function-like V33(b1 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) ) ) Function of b1 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) ) .: X : ( ( ) ( ) Element of b3 : ( ( non empty covering ) ( non empty covering ) Subset-Family of ) ) : ( ( ) ( ) set ) ) holds
f : ( ( Function-like V33(b1 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued Function-like V33(b1 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) ) ) Function of b1 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) ) is without_fixpoints ;

definition
let E be ( ( ) ( ) set ) ;
let f be ( ( Function-like V33(E : ( ( ) ( ) set ) ,E : ( ( ) ( ) set ) ) ) ( Relation-like E : ( ( ) ( ) set ) -defined E : ( ( ) ( ) set ) -valued Function-like V33(E : ( ( ) ( ) set ) ,E : ( ( ) ( ) set ) ) ) Function of E : ( ( ) ( ) set ) ,E : ( ( ) ( ) set ) ) ;
func =_ f -> ( ( V29(E : ( ( ) ( ) set ) ) V40() V45() ) ( Relation-like E : ( ( ) ( ) set ) -defined E : ( ( ) ( ) set ) -valued V29(E : ( ( ) ( ) set ) ) V38() V40() V45() ) Equivalence_Relation of ) means :: ABIAN:def 7
 for x, y being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in E : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in E : ( ( ) ( ) set ) holds
( [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in it : ( ( ) ( ) set ) iff ex k, l being ( ( ) ( ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) st (iter (f : ( ( non empty ) ( non empty ) set ) ,k : ( ( ) ( ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( Function-like V33(E : ( ( ) ( ) set ) ,E : ( ( ) ( ) set ) ) ) ( Relation-like E : ( ( ) ( ) set ) -defined E : ( ( ) ( ) set ) -valued Function-like V33(E : ( ( ) ( ) set ) ,E : ( ( ) ( ) set ) ) ) Function of E : ( ( ) ( ) set ) ,E : ( ( ) ( ) set ) ) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (iter (f : ( ( non empty ) ( non empty ) set ) ,l : ( ( ) ( ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( Function-like V33(E : ( ( ) ( ) set ) ,E : ( ( ) ( ) set ) ) ) ( Relation-like E : ( ( ) ( ) set ) -defined E : ( ( ) ( ) set ) -valued Function-like V33(E : ( ( ) ( ) set ) ,E : ( ( ) ( ) set ) ) ) Function of E : ( ( ) ( ) set ) ,E : ( ( ) ( ) set ) ) . y : ( ( ) ( ) set ) : ( ( ) ( ) set ) );
end;

theorem :: ABIAN:6
for E being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of E : ( ( non empty ) ( non empty ) set ) ,E : ( ( non empty ) ( non empty ) set ) )
for c being ( ( ) ( non empty ) Element of Class (=_ f : ( ( Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( V29(b1 : ( ( non empty ) ( non empty ) set ) ) V40() V45() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V29(b1 : ( ( non empty ) ( non empty ) set ) ) V38() V40() V45() ) Equivalence_Relation of ) : ( ( ) ( non empty with_non-empty_elements non empty-membered ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) )
for e being ( ( ) ( ) Element of c : ( ( ) ( non empty ) Element of Class (=_ b2 : ( ( Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( V29(b1 : ( ( non empty ) ( non empty ) set ) ) V40() V45() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V29(b1 : ( ( non empty ) ( non empty ) set ) ) V38() V40() V45() ) Equivalence_Relation of ) : ( ( ) ( non empty with_non-empty_elements non empty-membered ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) holds f : ( ( Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) . e : ( ( ) ( ) Element of b3 : ( ( ) ( non empty ) Element of Class (=_ b2 : ( ( Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( V29(b1 : ( ( non empty ) ( non empty ) set ) ) V40() V45() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V29(b1 : ( ( non empty ) ( non empty ) set ) ) V38() V40() V45() ) Equivalence_Relation of ) : ( ( ) ( non empty with_non-empty_elements non empty-membered ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) in c : ( ( ) ( non empty ) Element of Class (=_ b2 : ( ( Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( V29(b1 : ( ( non empty ) ( non empty ) set ) ) V40() V45() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V29(b1 : ( ( non empty ) ( non empty ) set ) ) V38() V40() V45() ) Equivalence_Relation of ) : ( ( ) ( non empty with_non-empty_elements non empty-membered ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ) ;

theorem :: ABIAN:7
for E being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of E : ( ( non empty ) ( non empty ) set ) ,E : ( ( non empty ) ( non empty ) set ) )
for c being ( ( ) ( non empty ) Element of Class (=_ f : ( ( Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( V29(b1 : ( ( non empty ) ( non empty ) set ) ) V40() V45() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V29(b1 : ( ( non empty ) ( non empty ) set ) ) V38() V40() V45() ) Equivalence_Relation of ) : ( ( ) ( non empty with_non-empty_elements non empty-membered ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) )
for e being ( ( ) ( ) Element of c : ( ( ) ( non empty ) Element of Class (=_ b2 : ( ( Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( V29(b1 : ( ( non empty ) ( non empty ) set ) ) V40() V45() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V29(b1 : ( ( non empty ) ( non empty ) set ) ) V38() V40() V45() ) Equivalence_Relation of ) : ( ( ) ( non empty with_non-empty_elements non empty-membered ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ) )
for n being ( ( ) ( ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) holds (iter (f : ( ( Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ,n : ( ( ) ( ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) . e : ( ( ) ( ) Element of b3 : ( ( ) ( non empty ) Element of Class (=_ b2 : ( ( Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( V29(b1 : ( ( non empty ) ( non empty ) set ) ) V40() V45() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V29(b1 : ( ( non empty ) ( non empty ) set ) ) V38() V40() V45() ) Equivalence_Relation of ) : ( ( ) ( non empty with_non-empty_elements non empty-membered ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) in c : ( ( ) ( non empty ) Element of Class (=_ b2 : ( ( Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( V29(b1 : ( ( non empty ) ( non empty ) set ) ) V40() V45() ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued V29(b1 : ( ( non empty ) ( non empty ) set ) ) V38() V40() V45() ) Equivalence_Relation of ) : ( ( ) ( non empty with_non-empty_elements non empty-membered ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ) ;

registration
cluster empty-membered -> trivial for ( ( ) ( ) set ) ;
end;

registration
let A be ( ( ) ( ) set ) ;
let B be ( ( with_non-empty_element ) ( non empty with_non-empty_element ) set ) ;
cluster Relation-like non-empty A : ( ( ) ( ) set ) -defined B : ( ( with_non-empty_element ) ( non empty with_non-empty_element ) set ) -valued Function-like V33(A : ( ( ) ( ) set ) ,B : ( ( with_non-empty_element ) ( non empty with_non-empty_element ) set ) ) for ( ( ) ( ) Element of bool [:A : ( ( ) ( ) set ) ,B : ( ( with_non-empty_element ) ( non empty with_non-empty_element ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
let A be ( ( non empty ) ( non empty ) set ) ;
let B be ( ( with_non-empty_element ) ( non empty with_non-empty_element ) set ) ;
let f be ( ( non-empty Function-like V33(A : ( ( non empty ) ( non empty ) set ) ,B : ( ( with_non-empty_element ) ( non empty with_non-empty_element ) set ) ) ) ( Relation-like non-empty A : ( ( non empty ) ( non empty ) set ) -defined B : ( ( with_non-empty_element ) ( non empty with_non-empty_element ) set ) -valued Function-like V33(A : ( ( non empty ) ( non empty ) set ) ,B : ( ( with_non-empty_element ) ( non empty with_non-empty_element ) set ) ) ) Function of A : ( ( non empty ) ( non empty ) set ) ,B : ( ( with_non-empty_element ) ( non empty with_non-empty_element ) set ) ) ;
let a be ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ;
cluster f : ( ( non-empty Function-like V33(A : ( ( non empty ) ( non empty ) set ) ,B : ( ( with_non-empty_element ) ( non empty with_non-empty_element ) set ) ) ) ( Relation-like non-empty A : ( ( non empty ) ( non empty ) set ) -defined B : ( ( with_non-empty_element ) ( non empty with_non-empty_element ) set ) -valued Function-like V33(A : ( ( non empty ) ( non empty ) set ) ,B : ( ( with_non-empty_element ) ( non empty with_non-empty_element ) set ) ) ) Element of bool [:A : ( ( non empty ) ( non empty ) set ) ,B : ( ( with_non-empty_element ) ( non empty with_non-empty_element ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . a : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) -> non empty ;
end;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
cluster bool X : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) -> with_non-empty_element ;
end;

theorem :: ABIAN:8
for E being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of E : ( ( non empty ) ( non empty ) set ) ,E : ( ( non empty ) ( non empty ) set ) ) st f : ( ( Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) is without_fixpoints holds
ex E1, E2, E3 being ( ( ) ( ) set ) st
( (E1 : ( ( ) ( ) set ) \/ E2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \/ E3 : ( ( ) ( ) set ) : ( ( ) ( ) set ) = E : ( ( non empty ) ( non empty ) set ) & f : ( ( Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) .: E1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) misses E1 : ( ( ) ( ) set ) & f : ( ( Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) .: E2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) misses E2 : ( ( ) ( ) set ) & f : ( ( Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) .: E3 : ( ( ) ( ) set ) : ( ( ) ( ) set ) misses E3 : ( ( ) ( ) set ) ) ;

begin

theorem :: ABIAN:9
for n being ( ( V16() ) ( ext-real V10() V11() V12() V16() complex V18() integer ) Nat) holds
( n : ( ( V16() ) ( ext-real V10() V11() V12() V16() complex V18() integer ) Nat) is odd iff ex k being ( ( ) ( ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) st n : ( ( V16() ) ( ext-real V10() V11() V12() V16() complex V18() integer ) Nat) = (2 : ( ( ) ( non empty ext-real positive non negative V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V74() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) * k : ( ( ) ( ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() even ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty ext-real positive non negative V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V74() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() odd ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: ABIAN:10
for n being ( ( ) ( ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) )
for A being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like V33(b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) ) Function of A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) )
for x being ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) holds (iter (f : ( ( Function-like V33(b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) ) Function of b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) ,(n : ( ( ) ( ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty ext-real positive non negative V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V74() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( Function-like V33(b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) ) Function of b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) = f : ( ( Function-like V33(b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) ) Function of b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) . ((iter (f : ( ( Function-like V33(b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) ) Function of b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) ,n : ( ( ) ( ext-real V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( Function-like V33(b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like V33(b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) ) Function of b2 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: ABIAN:11
for i being ( ( integer ) ( ext-real complex V18() integer ) Integer) holds
( i : ( ( integer ) ( ext-real complex V18() integer ) Integer) is even iff ex j being ( ( integer ) ( ext-real complex V18() integer ) Integer) st i : ( ( integer ) ( ext-real complex V18() integer ) Integer) = 2 : ( ( ) ( non empty ext-real positive non negative V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V74() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) * j : ( ( integer ) ( ext-real complex V18() integer ) Integer) : ( ( ) ( ext-real complex V18() integer even ) set ) ) ;

registration
cluster ext-real V10() V11() V12() V16() complex V18() integer odd for ( ( ) ( ) set ) ;
cluster ext-real V10() V11() V12() V16() complex V18() integer even for ( ( ) ( ) set ) ;
end;

theorem :: ABIAN:12
for n being ( ( V16() odd ) ( ext-real V10() V11() V12() V16() complex V18() integer odd ) Nat) holds 1 : ( ( ) ( non empty ext-real positive non negative V10() V11() V12() V16() complex V18() integer V57() V58() V59() V60() V61() V62() V63() V74() V76() ) Element of NAT : ( ( ) ( non empty V10() V11() V12() V58() V59() V60() V61() V62() V63() V64() V74() V76() ) Element of bool REAL : ( ( ) ( V58() V59() V60() V64() V76() V77() V79() ) set ) : ( ( ) ( non empty ) set ) ) ) <= n : ( ( V16() odd ) ( ext-real V10() V11() V12() V16() complex V18() integer odd ) Nat) ;

registration
cluster integer odd -> non zero integer for ( ( ) ( ) set ) ;
end;