:: ZF_FUND1 semantic presentation

begin

registration
let V be ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ;
cluster Relation-like for ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) ;
end;

definition
canceled;
let V be ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ;
let x, y be ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ;
:: original: (#)
redefine func x (#) y -> ( ( Relation-like ) ( Relation-like ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) ;
end;

definition
func decode -> ( ( Function-like quasi_total ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Function of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) , VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) means :: ZF_FUND1:def 2
 for p being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) holds it : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) . p : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) : ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) = x. (card p : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) : ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) ;
end;

definition
let v1 be ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) ;
func x". v1 -> ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) means :: ZF_FUND1:def 3
 x. it : ( ( ext-real ) ( ext-real ) set ) : ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) = v1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ;
end;

definition
let A be ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ;
func code A -> ( ( ) ( ) Subset of ( ( ) ( non trivial non finite ) set ) ) equals :: ZF_FUND1:def 4
(decode : ( ( Function-like quasi_total ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Function of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) , VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) ") : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) .: A : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) : ( ( ) ( ) set ) ;
end;

registration
let A be ( ( finite ) ( finite ) Subset of ( ( ) ( ) set ) ) ;
cluster code A : ( ( finite ) ( finite ) Element of bool VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non trivial non finite ) set ) ) -> finite ;
end;

definition
let H be ( ( ZF-formula-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) ZF-formula) ;
let E be ( ( non empty ) ( non empty ) set ) ;
func Diagram (H,E) -> ( ( ) ( ) set ) means :: ZF_FUND1:def 5
 for p being ( ( ) ( ) set ) holds
( p : ( ( ) ( ) set ) in it : ( ( ) ( ) set ) iff ex f being ( ( Function-like quasi_total ) ( Relation-like VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -defined E : ( ( ) ( ) set ) -valued Function-like non empty V14( VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) quasi_total ) Function of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ,E : ( ( ) ( ) set ) ) st
( p : ( ( ) ( ) set ) = (f : ( ( Function-like quasi_total ) ( Relation-like VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -defined E : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) quasi_total ) Function of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) * decode : ( ( Function-like quasi_total ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Function of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) , VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) ) : ( ( Function-like ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined E : ( ( ) ( ) set ) -valued E : ( ( non empty ) ( non empty ) set ) -valued Function-like ) Element of bool [:omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ,E : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) | (code (Free H : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) : ( ( ) ( ) Element of bool VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Subset of ( ( ) ( non trivial non finite ) set ) ) : ( ( Function-like ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined code (Free H : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) : ( ( ) ( ) Element of bool VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Subset of ( ( ) ( non trivial non finite ) set ) ) -defined omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined E : ( ( ) ( ) set ) -valued Function-like ) Element of bool [:omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ,E : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) & f : ( ( Function-like quasi_total ) ( Relation-like VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -defined E : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) quasi_total ) Function of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) in St (H : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ,E : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool (VAL E : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) );
end;

definition
let V be ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ;
let X be ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) ;
attr X is closed_wrt_A1 means :: ZF_FUND1:def 6
 for a being ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) st a : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in X : ( ( ) ( ) set ) holds
{ {[(0-element_of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) ,x : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ] : ( ( ) ( V22() ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) ,[(1-element_of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) : ( ( non empty ordinal ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) ,y : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ] : ( ( ) ( V22() ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) } : ( ( ) ( Relation-like finite ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) where x, y is ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) : ( x : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in y : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) & x : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in a : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) & y : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in a : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ) } in X : ( ( ) ( ) set ) ;
attr X is closed_wrt_A2 means :: ZF_FUND1:def 7
 for a, b being ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) st a : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in X : ( ( ) ( ) set ) & b : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in X : ( ( ) ( ) set ) holds
{a : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ,b : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) } : ( ( ) ( finite ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) in X : ( ( ) ( ) set ) ;
attr X is closed_wrt_A3 means :: ZF_FUND1:def 8
 for a being ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) st a : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in X : ( ( ) ( ) set ) holds
union a : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) in X : ( ( ) ( ) set ) ;
attr X is closed_wrt_A4 means :: ZF_FUND1:def 9
 for a, b being ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) st a : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in X : ( ( ) ( ) set ) & b : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in X : ( ( ) ( ) set ) holds
{ {[x : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ,y : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ] : ( ( ) ( V22() ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) } : ( ( ) ( Relation-like Function-like constant non empty trivial finite 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) -element ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) where x, y is ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) : ( x : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in a : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) & y : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in b : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ) } in X : ( ( ) ( ) set ) ;
attr X is closed_wrt_A5 means :: ZF_FUND1:def 10
 for a, b being ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) st a : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in X : ( ( ) ( ) set ) & b : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in X : ( ( ) ( ) set ) holds
{ (x : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) \/ y : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ) : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) where x, y is ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) : ( x : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in a : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) & y : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in b : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ) } in X : ( ( ) ( ) set ) ;
attr X is closed_wrt_A6 means :: ZF_FUND1:def 11
 for a, b being ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) st a : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in X : ( ( ) ( ) set ) & b : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in X : ( ( ) ( ) set ) holds
{ (x : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) \ y : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ) : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) where x, y is ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) : ( x : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in a : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) & y : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in b : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ) } in X : ( ( ) ( ) set ) ;
attr X is closed_wrt_A7 means :: ZF_FUND1:def 12
 for a, b being ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) st a : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in X : ( ( ) ( ) set ) & b : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in X : ( ( ) ( ) set ) holds
{ (x : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) (#) y : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ) : ( ( Relation-like ) ( Relation-like ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) where x, y is ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) set ) ) : ( x : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in a : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) & y : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in b : ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ) } in X : ( ( ) ( ) set ) ;
end;

definition
let V be ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ;
let X be ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) ;
attr X is closed_wrt_A1-A7 means :: ZF_FUND1:def 13
( X : ( ( ) ( ) set ) is closed_wrt_A1 & X : ( ( ) ( ) set ) is closed_wrt_A2 & X : ( ( ) ( ) set ) is closed_wrt_A3 & X : ( ( ) ( ) set ) is closed_wrt_A4 & X : ( ( ) ( ) set ) is closed_wrt_A5 & X : ( ( ) ( ) set ) is closed_wrt_A6 & X : ( ( ) ( ) set ) is closed_wrt_A7 );
end;

theorem :: ZF_FUND1:1
for V being ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe)
for X being ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) )
for o, A being ( ( ) ( ) set ) holds
( X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) c= V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) & ( o : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) implies o : ( ( ) ( ) set ) is ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ) & ( o : ( ( ) ( ) set ) in A : ( ( ) ( ) set ) & A : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) implies o : ( ( ) ( ) set ) is ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ) ) ;

theorem :: ZF_FUND1:2
for V being ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe)
for X being ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) )
for o, A being ( ( ) ( ) set ) st X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) is closed_wrt_A1-A7 holds
( ( o : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) implies {o : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) -element ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) ) & ( {o : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) -element ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) implies o : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) ) & ( A : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) implies union A : ( ( ) ( ) set ) : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) ) ) ;

theorem :: ZF_FUND1:3
for V being ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe)
for X being ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) st X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) is closed_wrt_A1-A7 holds
{} : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) ;

theorem :: ZF_FUND1:4
for V being ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe)
for X being ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) )
for A, B being ( ( ) ( ) set ) st X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) is closed_wrt_A1-A7 & A : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) & B : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) holds
( A : ( ( ) ( ) set ) \/ B : ( ( ) ( ) set ) : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) & A : ( ( ) ( ) set ) \ B : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool b3 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) & A : ( ( ) ( ) set ) (#) B : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) ) ;

theorem :: ZF_FUND1:5
for V being ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe)
for X being ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) )
for A, B being ( ( ) ( ) set ) st X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) is closed_wrt_A1-A7 & A : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) & B : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) holds
A : ( ( ) ( ) set ) /\ B : ( ( ) ( ) set ) : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) ;

theorem :: ZF_FUND1:6
for V being ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe)
for X being ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) )
for o, p being ( ( ) ( ) set ) st X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) is closed_wrt_A1-A7 & o : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) & p : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) holds
( {o : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) } : ( ( ) ( finite ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) & [o : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) ] : ( ( ) ( V22() ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) ) ;

theorem :: ZF_FUND1:7
for V being ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe)
for X being ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) st X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) is closed_wrt_A1-A7 holds
omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) c= X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) ;

theorem :: ZF_FUND1:8
for V being ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe)
for X being ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) )
for fs being ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) st X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) is closed_wrt_A1-A7 holds
Funcs (fs : ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) ,omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of b3 : ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) , omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) c= X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) ;

theorem :: ZF_FUND1:9
for V being ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe)
for a being ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) )
for X being ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) )
for fs being ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) st X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) is closed_wrt_A1-A7 & a : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) holds
Funcs (fs : ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) ,a : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ) : ( ( ) ( functional ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) ;

theorem :: ZF_FUND1:10
for V being ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe)
for a, b being ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) )
for X being ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) )
for fs being ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) st X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) is closed_wrt_A1-A7 & a : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in Funcs (fs : ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) ,omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of b5 : ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) , omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) & b : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) holds
{ (a : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) (#) x : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ) : ( ( Relation-like ) ( Relation-like ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) where x is ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) : x : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in b : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) } in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) ;

theorem :: ZF_FUND1:11
for V being ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe)
for a, b being ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) )
for X being ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) )
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) )
for fs being ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) st X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) is closed_wrt_A1-A7 & n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) in fs : ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) & a : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) & b : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) & b : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) c= Funcs (fs : ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) ,a : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ) : ( ( ) ( functional ) set ) holds
{ x : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) where x is ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) : ( x : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in Funcs ((fs : ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) \ {n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) } : ( ( ) ( non empty trivial finite V48() 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) -element ) Element of bool omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) : ( ( ) ( non trivial non finite ) set ) ) ) : ( ( ) ( finite ) Element of bool omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) : ( ( ) ( non trivial non finite ) set ) ) ,a : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ) : ( ( ) ( functional ) set ) & ex u being ( ( ) ( ) set ) st {[n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) ,u : ( ( ) ( ) set ) ] : ( ( ) ( V22() ) set ) } : ( ( ) ( Relation-like Function-like constant non empty trivial finite 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) -element ) set ) \/ x : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) : ( ( ) ( ) set ) in b : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ) } in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) ;

theorem :: ZF_FUND1:12
for V being ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe)
for a, b being ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) )
for X being ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) )
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) st X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) is closed_wrt_A1-A7 & a : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) & b : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) holds
{ ({[n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) ,x : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ] : ( ( ) ( V22() ) Element of [:omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ,b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) :] : ( ( ) ( Relation-like non trivial non finite ) set ) ) } : ( ( ) ( Relation-like Function-like constant non empty trivial finite 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) -element ) set ) \/ y : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ) : ( ( ) ( ) set ) where x, y is ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) : ( x : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in a : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) & y : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in b : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ) } in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) ;

theorem :: ZF_FUND1:13
for V being ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe)
for X being ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) )
for B being ( ( ) ( ) set ) st X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) is closed_wrt_A1-A7 & B : ( ( ) ( ) set ) is finite & ( for o being ( ( ) ( ) set ) st o : ( ( ) ( ) set ) in B : ( ( ) ( ) set ) holds
o : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) ) holds
B : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) ;

theorem :: ZF_FUND1:14
for V being ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe)
for y being ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) )
for X being ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) )
for A being ( ( ) ( ) set )
for fs being ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) st X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) is closed_wrt_A1-A7 & A : ( ( ) ( ) set ) c= X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) & y : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in Funcs (fs : ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) ,A : ( ( ) ( ) set ) ) : ( ( ) ( functional ) set ) holds
y : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) ;

theorem :: ZF_FUND1:15
for V being ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe)
for a, y being ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) )
for X being ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) )
for fs being ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) )
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) st X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) is closed_wrt_A1-A7 & a : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) & a : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) c= X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) & y : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in Funcs (fs : ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) ,a : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ) : ( ( ) ( functional ) set ) holds
{ ({[n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) ,x : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ] : ( ( ) ( V22() ) Element of [:omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ,b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) :] : ( ( ) ( Relation-like non trivial non finite ) set ) ) } : ( ( ) ( Relation-like Function-like constant non empty trivial finite 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) -element ) set ) \/ y : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ) : ( ( ) ( ) set ) where x is ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) : x : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in a : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) } in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) ;

theorem :: ZF_FUND1:16
for V being ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe)
for a, y, b being ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) )
for X being ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) )
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) )
for fs being ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) st X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) is closed_wrt_A1-A7 & not n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) in fs : ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) & a : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) & a : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) c= X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) & y : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in Funcs (fs : ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) ,a : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ) : ( ( ) ( functional ) set ) & b : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) c= Funcs ((fs : ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) \/ {n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) } : ( ( ) ( non empty trivial finite V48() 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) -element ) Element of bool omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) : ( ( ) ( non trivial non finite ) set ) ) ) : ( ( ) ( finite ) Element of bool omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) : ( ( ) ( non trivial non finite ) set ) ) ,a : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ) : ( ( ) ( functional ) set ) & b : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) holds
{ x : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) where x is ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) : ( x : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in a : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) & {[n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) ,x : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ] : ( ( ) ( V22() ) Element of [:omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ,b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) :] : ( ( ) ( Relation-like non trivial non finite ) set ) ) } : ( ( ) ( Relation-like Function-like constant non empty trivial finite 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) -element ) set ) \/ y : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) : ( ( ) ( ) set ) in b : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ) } in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) ;

theorem :: ZF_FUND1:17
for V being ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe)
for a being ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) )
for X being ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) st X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) is closed_wrt_A1-A7 & a : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) holds
{ {[(0-element_of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ,x : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ] : ( ( ) ( V22() ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ,[(1-element_of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) : ( ( non empty ordinal ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ,x : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) ] : ( ( ) ( V22() ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) } : ( ( ) ( Relation-like finite ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) where x is ( ( ) ( ) Element of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) : x : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in a : ( ( ) ( ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) } in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) ;

theorem :: ZF_FUND1:18
for V being ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe)
for X being ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) )
for E being ( ( non empty ) ( non empty ) set ) st X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) is closed_wrt_A1-A7 & E : ( ( non empty ) ( non empty ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) holds
for v1, v2 being ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) holds
( Diagram ((v1 : ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) '=' v2 : ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) M8( NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) )) ,E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) & Diagram ((v1 : ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) 'in' v2 : ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) M8( NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) )) ,E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) ) ;

theorem :: ZF_FUND1:19
for V being ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe)
for X being ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) )
for E being ( ( non empty ) ( non empty ) set ) st X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) is closed_wrt_A1-A7 & E : ( ( non empty ) ( non empty ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) holds
for H being ( ( ZF-formula-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) ZF-formula) st Diagram (H : ( ( ZF-formula-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) ZF-formula) ,E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) holds
Diagram (('not' H : ( ( ZF-formula-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) ZF-formula) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) M8( NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) )) ,E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) ;

theorem :: ZF_FUND1:20
for V being ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe)
for X being ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) )
for E being ( ( non empty ) ( non empty ) set ) st X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) is closed_wrt_A1-A7 & E : ( ( non empty ) ( non empty ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) holds
for H, H9 being ( ( ZF-formula-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) ZF-formula) st Diagram (H : ( ( ZF-formula-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) ZF-formula) ,E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) & Diagram (H9 : ( ( ZF-formula-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) ZF-formula) ,E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) holds
Diagram ((H : ( ( ZF-formula-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) ZF-formula) '&' H9 : ( ( ZF-formula-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) ZF-formula) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) M8( NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) )) ,E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) ;

theorem :: ZF_FUND1:21
for V being ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe)
for X being ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) )
for E being ( ( non empty ) ( non empty ) set ) st X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) is closed_wrt_A1-A7 & E : ( ( non empty ) ( non empty ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) holds
for H being ( ( ZF-formula-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) ZF-formula)
for v1 being ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) st Diagram (H : ( ( ZF-formula-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) ZF-formula) ,E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) holds
Diagram ((All (v1 : ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) ,H : ( ( ZF-formula-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) ZF-formula) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) M8( NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) )) ,E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) ;

theorem :: ZF_FUND1:22
for V being ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe)
for X being ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) )
for E being ( ( non empty ) ( non empty ) set )
for H being ( ( ZF-formula-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) ZF-formula) st X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) is closed_wrt_A1-A7 & E : ( ( non empty ) ( non empty ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) holds
Diagram (H : ( ( ZF-formula-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) ZF-formula) ,E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) ;

theorem :: ZF_FUND1:23
for V being ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe)
for X being ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) )
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) st X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) is closed_wrt_A1-A7 holds
( n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) & 0-element_of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) : ( ( ordinal ) ( epsilon-transitive epsilon-connected ordinal ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) & 1-element_of V : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) : ( ( non empty ordinal ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of b1 : ( ( non empty universal ) ( non empty epsilon-transitive V35() V36() universal ) Universe) ) in X : ( ( non empty ) ( non empty ) Subclass of ( ( ) ( ) set ) ) ) ;

theorem :: ZF_FUND1:24
for o, p, q being ( ( ) ( ) set ) holds {[o : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) ] : ( ( ) ( V22() ) set ) ,[p : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) ] : ( ( ) ( V22() ) set ) } : ( ( ) ( Relation-like finite ) set ) (#) {[p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) ] : ( ( ) ( V22() ) set ) } : ( ( ) ( Relation-like Function-like constant non empty trivial finite 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) -element ) set ) : ( ( Relation-like ) ( Relation-like ) set ) = {[o : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) ] : ( ( ) ( V22() ) set ) ,[p : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) ] : ( ( ) ( V22() ) set ) } : ( ( ) ( Relation-like finite ) set ) ;

theorem :: ZF_FUND1:25
for p, r, o, q, s, t being ( ( ) ( ) set ) st p : ( ( ) ( ) set ) <> r : ( ( ) ( ) set ) holds
{[o : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) ] : ( ( ) ( V22() ) set ) ,[q : ( ( ) ( ) set ) ,r : ( ( ) ( ) set ) ] : ( ( ) ( V22() ) set ) } : ( ( ) ( Relation-like finite ) set ) (#) {[p : ( ( ) ( ) set ) ,s : ( ( ) ( ) set ) ] : ( ( ) ( V22() ) set ) ,[r : ( ( ) ( ) set ) ,t : ( ( ) ( ) set ) ] : ( ( ) ( V22() ) set ) } : ( ( ) ( Relation-like finite ) set ) : ( ( Relation-like ) ( Relation-like ) set ) = {[o : ( ( ) ( ) set ) ,s : ( ( ) ( ) set ) ] : ( ( ) ( V22() ) set ) ,[q : ( ( ) ( ) set ) ,t : ( ( ) ( ) set ) ] : ( ( ) ( V22() ) set ) } : ( ( ) ( Relation-like finite ) set ) ;

theorem :: ZF_FUND1:26
for v1, v2 being ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) holds
( code {v1 : ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) -element ) Element of bool VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) = {(x". v1 : ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( non empty trivial finite V48() 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) & code {v1 : ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) ,v2 : ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) } : ( ( ) ( finite ) Element of bool VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) = {(x". v1 : ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ,(x". v2 : ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( finite V48() ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) ;

theorem :: ZF_FUND1:27
for o, q being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) holds
( dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = {o : ( ( ) ( ) set ) ,q : ( ( ) ( ) set ) } : ( ( ) ( finite ) set ) iff f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) = {[o : ( ( ) ( ) set ) ,(f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . o : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ] : ( ( ) ( V22() ) set ) ,[q : ( ( ) ( ) set ) ,(f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . q : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ] : ( ( ) ( V22() ) set ) } : ( ( ) ( Relation-like finite ) set ) ) ;

theorem :: ZF_FUND1:28
( dom decode : ( ( Function-like quasi_total ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Function of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) , VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) : ( ( ) ( non empty ) Element of bool omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) : ( ( ) ( non trivial non finite ) set ) ) = omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) & rng decode : ( ( Function-like quasi_total ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Function of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) , VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) : ( ( ) ( non empty ) Element of bool VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) : ( ( ) ( ) set ) ) = VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) & decode : ( ( Function-like quasi_total ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Function of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) , VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) is one-to-one & decode : ( ( Function-like quasi_total ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Function of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) , VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) " : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) is one-to-one & dom (decode : ( ( Function-like quasi_total ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Function of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) , VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) ") : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) = VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) & rng (decode : ( ( Function-like quasi_total ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Function of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) , VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) ") : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) = omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) ;

theorem :: ZF_FUND1:29
for A being ( ( finite ) ( finite ) Subset of ( ( ) ( ) set ) ) holds A : ( ( finite ) ( finite ) Subset of ( ( ) ( ) set ) ) , code A : ( ( finite ) ( finite ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) are_equipotent ;

theorem :: ZF_FUND1:30
for A being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) holds A : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) = x". (x. (card A : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) ) : ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: ZF_FUND1:31
for fs being ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) )
for E being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like quasi_total ) ( Relation-like VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) quasi_total ) Function of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) holds
( dom ((f : ( ( Function-like quasi_total ) ( Relation-like VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) quasi_total ) Function of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ,b2 : ( ( non empty ) ( non empty ) set ) ) * decode : ( ( Function-like quasi_total ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Function of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) , VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) ) : ( ( Function-like ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Element of bool [:omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like non trivial non finite ) set ) : ( ( ) ( non trivial non finite ) set ) ) | fs : ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) ) : ( ( Function-like ) ( Relation-like b1 : ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) -defined omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like finite ) Element of bool [:omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like non trivial non finite ) set ) : ( ( ) ( non trivial non finite ) set ) ) : ( ( ) ( finite ) Element of bool b1 : ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) : ( ( ) ( finite V48() ) set ) ) = fs : ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) & rng ((f : ( ( Function-like quasi_total ) ( Relation-like VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) quasi_total ) Function of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ,b2 : ( ( non empty ) ( non empty ) set ) ) * decode : ( ( Function-like quasi_total ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Function of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) , VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) ) : ( ( Function-like ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Element of bool [:omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like non trivial non finite ) set ) : ( ( ) ( non trivial non finite ) set ) ) | fs : ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) ) : ( ( Function-like ) ( Relation-like b1 : ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) -defined omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like finite ) Element of bool [:omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like non trivial non finite ) set ) : ( ( ) ( non trivial non finite ) set ) ) : ( ( ) ( finite ) Element of bool b2 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) c= E : ( ( non empty ) ( non empty ) set ) & (f : ( ( Function-like quasi_total ) ( Relation-like VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) quasi_total ) Function of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ,b2 : ( ( non empty ) ( non empty ) set ) ) * decode : ( ( Function-like quasi_total ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Function of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) , VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) ) : ( ( Function-like ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Element of bool [:omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like non trivial non finite ) set ) : ( ( ) ( non trivial non finite ) set ) ) | fs : ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) : ( ( Function-like ) ( Relation-like b1 : ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) -defined omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like finite ) Element of bool [:omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like non trivial non finite ) set ) : ( ( ) ( non trivial non finite ) set ) ) in Funcs (fs : ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of b1 : ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) ,b2 : ( ( non empty ) ( non empty ) set ) ) & dom (f : ( ( Function-like quasi_total ) ( Relation-like VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) quasi_total ) Function of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ,b2 : ( ( non empty ) ( non empty ) set ) ) * decode : ( ( Function-like quasi_total ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Function of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) , VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) ) : ( ( Function-like ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Element of bool [:omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like non trivial non finite ) set ) : ( ( ) ( non trivial non finite ) set ) ) : ( ( ) ( non empty ) Element of bool omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) : ( ( ) ( non trivial non finite ) set ) ) = omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) ;

theorem :: ZF_FUND1:32
for E being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like quasi_total ) ( Relation-like VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) quasi_total ) Function of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) )
for v1 being ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) holds
( decode : ( ( Function-like quasi_total ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Function of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) , VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) . (x". v1 : ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) = v1 : ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) & (decode : ( ( Function-like quasi_total ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Function of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) , VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) ") : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) . v1 : ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) : ( ( ) ( ) set ) = x". v1 : ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) & (f : ( ( Function-like quasi_total ) ( Relation-like VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) quasi_total ) Function of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) * decode : ( ( Function-like quasi_total ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Function of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) , VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) ) : ( ( Function-like ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Element of bool [:omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like non trivial non finite ) set ) : ( ( ) ( non trivial non finite ) set ) ) . (x". v1 : ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) = f : ( ( Function-like quasi_total ) ( Relation-like VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) quasi_total ) Function of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) . v1 : ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) ;

theorem :: ZF_FUND1:33
for p being ( ( ) ( ) set )
for A being ( ( finite ) ( finite ) Subset of ( ( ) ( ) set ) ) holds
( p : ( ( ) ( ) set ) in code A : ( ( finite ) ( finite ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) iff ex v1 being ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) st
( v1 : ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) in A : ( ( finite ) ( finite ) Subset of ( ( ) ( ) set ) ) & p : ( ( ) ( ) set ) = x". v1 : ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) ) ;

theorem :: ZF_FUND1:34
for A, B being ( ( finite ) ( finite ) Subset of ( ( ) ( ) set ) ) holds
( code (A : ( ( finite ) ( finite ) Subset of ( ( ) ( ) set ) ) \/ B : ( ( finite ) ( finite ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( finite ) Element of bool VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) = (code A : ( ( finite ) ( finite ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) \/ (code B : ( ( finite ) ( finite ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) : ( ( ) ( finite ) Element of bool omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) : ( ( ) ( non trivial non finite ) set ) ) & code (A : ( ( finite ) ( finite ) Subset of ( ( ) ( ) set ) ) \ B : ( ( finite ) ( finite ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( finite ) Element of bool VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) = (code A : ( ( finite ) ( finite ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) \ (code B : ( ( finite ) ( finite ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) : ( ( ) ( finite ) Element of bool omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) : ( ( ) ( non trivial non finite ) set ) ) ) ;

theorem :: ZF_FUND1:35
for E being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like quasi_total ) ( Relation-like VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) quasi_total ) Function of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) )
for v1 being ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) )
for H being ( ( ZF-formula-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) ZF-formula) st v1 : ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) in Free H : ( ( ZF-formula-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) ZF-formula) : ( ( ) ( finite ) Element of bool VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) : ( ( ) ( ) set ) ) holds
((f : ( ( Function-like quasi_total ) ( Relation-like VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) quasi_total ) Function of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) * decode : ( ( Function-like quasi_total ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Function of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) , VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) ) : ( ( Function-like ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Element of bool [:omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like non trivial non finite ) set ) : ( ( ) ( non trivial non finite ) set ) ) | (code (Free H : ( ( ZF-formula-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) ZF-formula) ) : ( ( ) ( finite ) Element of bool VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) ) : ( ( Function-like ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined code (Free b4 : ( ( ZF-formula-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) ZF-formula) ) : ( ( ) ( finite ) Element of bool VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) -defined omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like finite ) Element of bool [:omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like non trivial non finite ) set ) : ( ( ) ( non trivial non finite ) set ) ) . (x". v1 : ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural ext-real V33() V34() finite cardinal ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) = f : ( ( Function-like quasi_total ) ( Relation-like VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) quasi_total ) Function of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) . v1 : ( ( ) ( ) Element of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: ZF_FUND1:36
for E being ( ( non empty ) ( non empty ) set )
for H being ( ( ZF-formula-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) ZF-formula)
for f, g being ( ( Function-like quasi_total ) ( Relation-like VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) quasi_total ) Function of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) st (f : ( ( Function-like quasi_total ) ( Relation-like VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) quasi_total ) Function of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) * decode : ( ( Function-like quasi_total ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Function of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) , VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) ) : ( ( Function-like ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Element of bool [:omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like non trivial non finite ) set ) : ( ( ) ( non trivial non finite ) set ) ) | (code (Free H : ( ( ZF-formula-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) ZF-formula) ) : ( ( ) ( finite ) Element of bool VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) : ( ( Function-like ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined code (Free b2 : ( ( ZF-formula-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) ZF-formula) ) : ( ( ) ( finite ) Element of bool VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) -defined omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like finite ) Element of bool [:omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like non trivial non finite ) set ) : ( ( ) ( non trivial non finite ) set ) ) = (g : ( ( Function-like quasi_total ) ( Relation-like VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) quasi_total ) Function of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) * decode : ( ( Function-like quasi_total ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Function of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) , VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) ) : ( ( Function-like ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Element of bool [:omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like non trivial non finite ) set ) : ( ( ) ( non trivial non finite ) set ) ) | (code (Free H : ( ( ZF-formula-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) ZF-formula) ) : ( ( ) ( finite ) Element of bool VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) : ( ( Function-like ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined code (Free b2 : ( ( ZF-formula-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) ZF-formula) ) : ( ( ) ( finite ) Element of bool VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) -defined omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like finite ) Element of bool [:omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like non trivial non finite ) set ) : ( ( ) ( non trivial non finite ) set ) ) & f : ( ( Function-like quasi_total ) ( Relation-like VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) quasi_total ) Function of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) in St (H : ( ( ZF-formula-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) ZF-formula) ,E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool (VAL b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) holds
g : ( ( Function-like quasi_total ) ( Relation-like VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) quasi_total ) Function of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) in St (H : ( ( ZF-formula-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) -valued Function-like V52() ZF-formula-like ) ZF-formula) ,E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool (VAL b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;

theorem :: ZF_FUND1:37
for p being ( ( ) ( ) set )
for fs being ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) )
for E being ( ( non empty ) ( non empty ) set ) st p : ( ( ) ( ) set ) in Funcs (fs : ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of b2 : ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) ,b3 : ( ( non empty ) ( non empty ) set ) ) holds
ex f being ( ( Function-like quasi_total ) ( Relation-like VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -defined b3 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) quasi_total ) Function of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) st p : ( ( ) ( ) set ) = (f : ( ( Function-like quasi_total ) ( Relation-like VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -defined b3 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) quasi_total ) Function of VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ,b3 : ( ( non empty ) ( non empty ) set ) ) * decode : ( ( Function-like quasi_total ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Function of omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) , VAR : ( ( ) ( non empty ) Element of bool NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non trivial non finite ) set ) ) ) ) : ( ( Function-like ) ( Relation-like omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty V14( omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ) quasi_total ) Element of bool [:omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like non trivial non finite ) set ) : ( ( ) ( non trivial non finite ) set ) ) | fs : ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) : ( ( Function-like ) ( Relation-like b2 : ( ( finite ) ( finite ) Subset of ( ( ) ( non trivial non finite ) set ) ) -defined omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -valued Function-like finite ) Element of bool [:omega : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal ) set ) ,b3 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( Relation-like non trivial non finite ) set ) : ( ( ) ( non trivial non finite ) set ) ) ;