:: ZFMODEL1 semantic presentation

begin

theorem :: ZFMODEL1:1
for E being ( ( non empty ) ( non empty ) set ) st E : ( ( non empty ) ( non empty ) set ) is epsilon-transitive holds
E : ( ( non empty ) ( non empty ) set ) |= the_axiom_of_extensionality : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: ZFMODEL1:2
for E being ( ( non empty ) ( non empty ) set ) st E : ( ( non empty ) ( non empty ) set ) is epsilon-transitive holds
( E : ( ( non empty ) ( non empty ) set ) |= the_axiom_of_pairs : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) iff for u, v being ( ( ) ( ) Element of E : ( ( non empty ) ( non empty ) set ) ) holds {u : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,v : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( ) set ) in E : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: ZFMODEL1:3
for E being ( ( non empty ) ( non empty ) set ) st E : ( ( non empty ) ( non empty ) set ) is epsilon-transitive holds
( E : ( ( non empty ) ( non empty ) set ) |= the_axiom_of_pairs : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) iff for X, Y being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) in E : ( ( non empty ) ( non empty ) set ) & Y : ( ( ) ( ) set ) in E : ( ( non empty ) ( non empty ) set ) holds
{X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) } : ( ( ) ( ) set ) in E : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: ZFMODEL1:4
for E being ( ( non empty ) ( non empty ) set ) st E : ( ( non empty ) ( non empty ) set ) is epsilon-transitive holds
( E : ( ( non empty ) ( non empty ) set ) |= the_axiom_of_unions : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) iff for u being ( ( ) ( ) Element of E : ( ( non empty ) ( non empty ) set ) ) holds union u : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) in E : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: ZFMODEL1:5
for E being ( ( non empty ) ( non empty ) set ) st E : ( ( non empty ) ( non empty ) set ) is epsilon-transitive holds
( E : ( ( non empty ) ( non empty ) set ) |= the_axiom_of_unions : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) iff for X being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) in E : ( ( non empty ) ( non empty ) set ) holds
union X : ( ( ) ( ) set ) : ( ( ) ( ) set ) in E : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: ZFMODEL1:6
for E being ( ( non empty ) ( non empty ) set ) st E : ( ( non empty ) ( non empty ) set ) is epsilon-transitive holds
( E : ( ( non empty ) ( non empty ) set ) |= the_axiom_of_infinity : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) iff ex u being ( ( ) ( ) Element of E : ( ( non empty ) ( non empty ) set ) ) st
( u : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) <> {} : ( ( ) ( ) set ) & ( for v being ( ( ) ( ) Element of E : ( ( non empty ) ( non empty ) set ) ) st v : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) in u : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) holds
ex w being ( ( ) ( ) Element of E : ( ( non empty ) ( non empty ) set ) ) st
( v : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) c< w : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) & w : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) in u : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) ) ) ;

theorem :: ZFMODEL1:7
for E being ( ( non empty ) ( non empty ) set ) st E : ( ( non empty ) ( non empty ) set ) is epsilon-transitive holds
( E : ( ( non empty ) ( non empty ) set ) |= the_axiom_of_infinity : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) iff ex X being ( ( ) ( ) set ) st
( X : ( ( ) ( ) set ) in E : ( ( non empty ) ( non empty ) set ) & X : ( ( ) ( ) set ) <> {} : ( ( ) ( ) set ) & ( for Y being ( ( ) ( ) set ) st Y : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) holds
ex Z being ( ( ) ( ) set ) st
( Y : ( ( ) ( ) set ) c< Z : ( ( ) ( ) set ) & Z : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) ) ) ) ) ;

theorem :: ZFMODEL1:8
for E being ( ( non empty ) ( non empty ) set ) st E : ( ( non empty ) ( non empty ) set ) is epsilon-transitive holds
( E : ( ( non empty ) ( non empty ) set ) |= the_axiom_of_power_sets : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) iff for u being ( ( ) ( ) Element of E : ( ( non empty ) ( non empty ) set ) ) holds E : ( ( non empty ) ( non empty ) set ) /\ (bool u : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) in E : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: ZFMODEL1:9
for E being ( ( non empty ) ( non empty ) set ) st E : ( ( non empty ) ( non empty ) set ) is epsilon-transitive holds
( E : ( ( non empty ) ( non empty ) set ) |= the_axiom_of_power_sets : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) iff for X being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) in E : ( ( non empty ) ( non empty ) set ) holds
E : ( ( non empty ) ( non empty ) set ) /\ (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) in E : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: ZFMODEL1:10
for x being ( ( ) ( ext-real natural V14() ) Variable)
for H being ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula)
for E being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b3 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b3 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b3 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) st not x : ( ( ) ( ext-real natural V14() ) Variable) in Free H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) : ( ( ) ( V32() V33() V34() V35() V36() V37() ) Element of bool VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & E : ( ( non empty ) ( non empty ) set ) ,f : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b3 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b3 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b3 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b3 : ( ( non empty ) ( non empty ) set ) ) |= H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) holds
E : ( ( non empty ) ( non empty ) set ) ,f : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b3 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b3 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b3 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b3 : ( ( non empty ) ( non empty ) set ) ) |= All (x : ( ( ) ( ext-real natural V14() ) Variable) ,H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) ) : ( ( ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: ZFMODEL1:11
for x, y being ( ( ) ( ext-real natural V14() ) Variable)
for H being ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula)
for E being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b4 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) st {x : ( ( ) ( ext-real natural V14() ) Variable) ,y : ( ( ) ( ext-real natural V14() ) Variable) } : ( ( ) ( V32() V33() V34() V35() V36() V37() ) set ) misses Free H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) : ( ( ) ( V32() V33() V34() V35() V36() V37() ) Element of bool VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & E : ( ( non empty ) ( non empty ) set ) ,f : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b4 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) ) |= H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) holds
E : ( ( non empty ) ( non empty ) set ) ,f : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b4 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b4 : ( ( non empty ) ( non empty ) set ) ) |= All (x : ( ( ) ( ext-real natural V14() ) Variable) ,y : ( ( ) ( ext-real natural V14() ) Variable) ,H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) ) : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: ZFMODEL1:12
for x, y, z being ( ( ) ( ext-real natural V14() ) Variable)
for H being ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula)
for E being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b5 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b5 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b5 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) st {x : ( ( ) ( ext-real natural V14() ) Variable) ,y : ( ( ) ( ext-real natural V14() ) Variable) ,z : ( ( ) ( ext-real natural V14() ) Variable) } : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) set ) misses Free H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) : ( ( ) ( V32() V33() V34() V35() V36() V37() ) Element of bool VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & E : ( ( non empty ) ( non empty ) set ) ,f : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b5 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b5 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b5 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b5 : ( ( non empty ) ( non empty ) set ) ) |= H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) holds
E : ( ( non empty ) ( non empty ) set ) ,f : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b5 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b5 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b5 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b5 : ( ( non empty ) ( non empty ) set ) ) |= All (x : ( ( ) ( ext-real natural V14() ) Variable) ,y : ( ( ) ( ext-real natural V14() ) Variable) ,z : ( ( ) ( ext-real natural V14() ) Variable) ,H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) ) : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ;

definition
let H be ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) ;
let E be ( ( non empty ) ( non empty ) set ) ;
let val be ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined E : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) ;
assume that
not x. 0 : ( ( ) ( ext-real natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) in Free H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) : ( ( ) ( V32() V33() V34() V35() V36() V37() ) Element of bool VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) and
E : ( ( non empty ) ( non empty ) set ) ,val : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined E : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) |= All ((x. 3 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(Ex ((x. 0 : ( ( ) ( ext-real natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(All ((x. 4 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) <=> ((x. 4 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) '=' (x. 0 : ( ( ) ( ext-real natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ;
func def_func' (H,val) -> ( ( Function-like V29(E : ( ( ) ( ) set ) ,E : ( ( ) ( ) set ) ) ) ( Relation-like E : ( ( ) ( ) set ) -defined E : ( ( ) ( ) set ) -valued Function-like V29(E : ( ( ) ( ) set ) ,E : ( ( ) ( ) set ) ) ) Function of E : ( ( ) ( ) set ) ,E : ( ( ) ( ) set ) ) means :: ZFMODEL1:def 1
 for g being ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( ) ( ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined E : ( ( ) ( ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( ) ( ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( ) ( ) set ) ) st ( for y being ( ( ) ( ext-real natural V14() ) Variable) holds
( not g : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined E : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) . y : ( ( ) ( ext-real natural V14() ) Variable) : ( ( ) ( ) Element of E : ( ( ) ( ) set ) ) <> val : ( ( ) ( ) set ) . y : ( ( ) ( ext-real natural V14() ) Variable) : ( ( ) ( ) Element of E : ( ( ) ( ) set ) ) or x. 0 : ( ( ) ( ext-real natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) = y : ( ( ) ( ext-real natural V14() ) Variable) or x. 3 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) = y : ( ( ) ( ext-real natural V14() ) Variable) or x. 4 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) = y : ( ( ) ( ext-real natural V14() ) Variable) ) ) holds
( E : ( ( ) ( ) set ) ,g : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined E : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) |= H : ( ( ) ( ) set ) iff it : ( ( ) ( ) set ) . (g : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined E : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) . (x. 3 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of E : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of E : ( ( ) ( ) set ) ) = g : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined E : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) . (x. 4 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of E : ( ( ) ( ) set ) ) );
end;

theorem :: ZFMODEL1:13
for E being ( ( non empty ) ( non empty ) set )
for H being ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula)
for f, g being ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) st ( for x being ( ( ) ( ext-real natural V14() ) Variable) st f : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) . x : ( ( ) ( ext-real natural V14() ) Variable) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) <> g : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) . x : ( ( ) ( ext-real natural V14() ) Variable) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) holds
not x : ( ( ) ( ext-real natural V14() ) Variable) in Free H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) : ( ( ) ( V32() V33() V34() V35() V36() V37() ) Element of bool VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) & E : ( ( non empty ) ( non empty ) set ) ,f : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) |= H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) holds
E : ( ( non empty ) ( non empty ) set ) ,g : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) |= H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) ;

definition
let H be ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) ;
let E be ( ( non empty ) ( non empty ) set ) ;
assume that
Free H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) : ( ( ) ( V32() V33() V34() V35() V36() V37() ) Element of bool VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) c= {(x. 3 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(x. 4 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( V32() V33() V34() V35() V36() V37() ) set ) and
E : ( ( non empty ) ( non empty ) set ) |= All ((x. 3 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(Ex ((x. 0 : ( ( ) ( ext-real natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(All ((x. 4 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) <=> ((x. 4 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) '=' (x. 0 : ( ( ) ( ext-real natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ;
func def_func (H,E) -> ( ( Function-like V29(E : ( ( ) ( ) set ) ,E : ( ( ) ( ) set ) ) ) ( Relation-like E : ( ( ) ( ) set ) -defined E : ( ( ) ( ) set ) -valued Function-like V29(E : ( ( ) ( ) set ) ,E : ( ( ) ( ) set ) ) ) Function of E : ( ( ) ( ) set ) ,E : ( ( ) ( ) set ) ) means :: ZFMODEL1:def 2
 for g being ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( ) ( ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined E : ( ( ) ( ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( ) ( ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( ) ( ) set ) ) holds
( E : ( ( ) ( ) set ) ,g : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined E : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) |= H : ( ( ) ( ) set ) iff it : ( ( ) ( ) set ) . (g : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined E : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) . (x. 3 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of E : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of E : ( ( ) ( ) set ) ) = g : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined E : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) . (x. 4 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of E : ( ( ) ( ) set ) ) );
end;

definition
let F be ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;
let E be ( ( non empty ) ( non empty ) set ) ;
pred F is_definable_in E means :: ZFMODEL1:def 3
 ex H being ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) st
( Free H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) : ( ( ) ( V32() V33() V34() V35() V36() V37() ) Element of bool VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) c= {(x. 3 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(x. 4 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( V32() V33() V34() V35() V36() V37() ) set ) & E : ( ( ) ( ) set ) |= All ((x. 3 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(Ex ((x. 0 : ( ( ) ( ext-real natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(All ((x. 4 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) <=> ((x. 4 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) '=' (x. 0 : ( ( ) ( ext-real natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) & F : ( ( ) ( ) set ) = def_func (H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) ,E : ( ( ) ( ) set ) ) : ( ( Function-like V29(E : ( ( ) ( ) set ) ,E : ( ( ) ( ) set ) ) ) ( Relation-like E : ( ( ) ( ) set ) -defined E : ( ( ) ( ) set ) -valued Function-like V29(E : ( ( ) ( ) set ) ,E : ( ( ) ( ) set ) ) ) Function of E : ( ( ) ( ) set ) ,E : ( ( ) ( ) set ) ) );
pred F is_parametrically_definable_in E means :: ZFMODEL1:def 4
 ex H being ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) ex f being ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( ) ( ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined E : ( ( ) ( ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( ) ( ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( ) ( ) set ) ) st
( {(x. 0 : ( ( ) ( ext-real natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(x. 1 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(x. 2 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) set ) misses Free H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) : ( ( ) ( V32() V33() V34() V35() V36() V37() ) Element of bool VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & E : ( ( ) ( ) set ) ,f : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined E : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) |= All ((x. 3 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(Ex ((x. 0 : ( ( ) ( ext-real natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(All ((x. 4 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) <=> ((x. 4 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) '=' (x. 0 : ( ( ) ( ext-real natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) & F : ( ( ) ( ) set ) = def_func' (H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) ,f : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined E : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like V29(E : ( ( ) ( ) set ) ,E : ( ( ) ( ) set ) ) ) ( Relation-like E : ( ( ) ( ) set ) -defined E : ( ( ) ( ) set ) -valued Function-like V29(E : ( ( ) ( ) set ) ,E : ( ( ) ( ) set ) ) ) Function of E : ( ( ) ( ) set ) ,E : ( ( ) ( ) set ) ) );
end;

theorem :: ZFMODEL1:14
for E being ( ( non empty ) ( non empty ) set )
for F being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is_definable_in E : ( ( non empty ) ( non empty ) set ) holds
F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is_parametrically_definable_in E : ( ( non empty ) ( non empty ) set ) ;

theorem :: ZFMODEL1:15
for E being ( ( non empty ) ( non empty ) set ) st E : ( ( non empty ) ( non empty ) set ) is epsilon-transitive holds
( ( for H being ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) st {(x. 0 : ( ( ) ( ext-real natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(x. 1 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(x. 2 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) set ) misses Free H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) : ( ( ) ( V32() V33() V34() V35() V36() V37() ) Element of bool VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) holds
E : ( ( non empty ) ( non empty ) set ) |= the_axiom_of_substitution_for H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) iff for H being ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula)
for f being ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) st {(x. 0 : ( ( ) ( ext-real natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(x. 1 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(x. 2 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) set ) misses Free H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) : ( ( ) ( V32() V33() V34() V35() V36() V37() ) Element of bool VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & E : ( ( non empty ) ( non empty ) set ) ,f : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) |= All ((x. 3 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(Ex ((x. 0 : ( ( ) ( ext-real natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(All ((x. 4 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) <=> ((x. 4 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) '=' (x. 0 : ( ( ) ( ext-real natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
for u being ( ( ) ( ) Element of E : ( ( non empty ) ( non empty ) set ) ) holds (def_func' (H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) ,f : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) )) : ( ( Function-like V29(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) .: u : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in E : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: ZFMODEL1:16
for E being ( ( non empty ) ( non empty ) set ) st E : ( ( non empty ) ( non empty ) set ) is epsilon-transitive holds
( ( for H being ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) st {(x. 0 : ( ( ) ( ext-real natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(x. 1 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(x. 2 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) set ) misses Free H : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( V32() V33() V34() V35() V36() V37() ) Element of bool VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) holds
E : ( ( non empty ) ( non empty ) set ) |= the_axiom_of_substitution_for H : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) iff for F being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is_parametrically_definable_in E : ( ( non empty ) ( non empty ) set ) holds
for X being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) in E : ( ( non empty ) ( non empty ) set ) holds
F : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) .: X : ( ( ) ( ) set ) : ( ( ) ( ) set ) in E : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: ZFMODEL1:17
for E being ( ( non empty ) ( non empty ) set ) st E : ( ( non empty ) ( non empty ) set ) is being_a_model_of_ZF holds
( E : ( ( non empty ) ( non empty ) set ) is epsilon-transitive & ( for u, v being ( ( ) ( ) Element of E : ( ( non empty ) ( non empty ) set ) ) st ( for w being ( ( ) ( ) Element of E : ( ( non empty ) ( non empty ) set ) ) holds
( w : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) in u : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) iff w : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) in v : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ) holds
u : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) = v : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) & ( for u, v being ( ( ) ( ) Element of E : ( ( non empty ) ( non empty ) set ) ) holds {u : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) ,v : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( ) set ) in E : ( ( non empty ) ( non empty ) set ) ) & ( for u being ( ( ) ( ) Element of E : ( ( non empty ) ( non empty ) set ) ) holds union u : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) : ( ( ) ( ) set ) in E : ( ( non empty ) ( non empty ) set ) ) & ex u being ( ( ) ( ) Element of E : ( ( non empty ) ( non empty ) set ) ) st
( u : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) <> {} : ( ( ) ( ) set ) & ( for v being ( ( ) ( ) Element of E : ( ( non empty ) ( non empty ) set ) ) st v : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) in u : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) holds
ex w being ( ( ) ( ) Element of E : ( ( non empty ) ( non empty ) set ) ) st
( v : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) c< w : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) & w : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) in u : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) ) ) ) & ( for u being ( ( ) ( ) Element of E : ( ( non empty ) ( non empty ) set ) ) holds E : ( ( non empty ) ( non empty ) set ) /\ (bool u : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) in E : ( ( non empty ) ( non empty ) set ) ) & ( for H being ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula)
for f being ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) st {(x. 0 : ( ( ) ( ext-real natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(x. 1 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(x. 2 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) set ) misses Free H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) : ( ( ) ( V32() V33() V34() V35() V36() V37() ) Element of bool VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & E : ( ( non empty ) ( non empty ) set ) ,f : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) |= All ((x. 3 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(Ex ((x. 0 : ( ( ) ( ext-real natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(All ((x. 4 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) <=> ((x. 4 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) '=' (x. 0 : ( ( ) ( ext-real natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
for u being ( ( ) ( ) Element of E : ( ( non empty ) ( non empty ) set ) ) holds (def_func' (H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) ,f : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) )) : ( ( Function-like V29(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) .: u : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in E : ( ( non empty ) ( non empty ) set ) ) ) ;

theorem :: ZFMODEL1:18
for E being ( ( non empty ) ( non empty ) set ) st E : ( ( non empty ) ( non empty ) set ) is epsilon-transitive & ( for u, v being ( ( ) ( ) Element of E : ( ( non empty ) ( non empty ) set ) ) holds {u : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) ,v : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( ) set ) in E : ( ( non empty ) ( non empty ) set ) ) & ( for u being ( ( ) ( ) Element of E : ( ( non empty ) ( non empty ) set ) ) holds union u : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) : ( ( ) ( ) set ) in E : ( ( non empty ) ( non empty ) set ) ) & ex u being ( ( ) ( ) Element of E : ( ( non empty ) ( non empty ) set ) ) st
( u : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) <> {} : ( ( ) ( ) set ) & ( for v being ( ( ) ( ) Element of E : ( ( non empty ) ( non empty ) set ) ) st v : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) in u : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) holds
ex w being ( ( ) ( ) Element of E : ( ( non empty ) ( non empty ) set ) ) st
( v : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) c< w : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) & w : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) in u : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) ) ) ) & ( for u being ( ( ) ( ) Element of E : ( ( non empty ) ( non empty ) set ) ) holds E : ( ( non empty ) ( non empty ) set ) /\ (bool u : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) in E : ( ( non empty ) ( non empty ) set ) ) & ( for H being ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula)
for f being ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,E : ( ( non empty ) ( non empty ) set ) ) st {(x. 0 : ( ( ) ( ext-real natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(x. 1 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(x. 2 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) } : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) set ) misses Free H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) : ( ( ) ( V32() V33() V34() V35() V36() V37() ) Element of bool VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & E : ( ( non empty ) ( non empty ) set ) ,f : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) |= All ((x. 3 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(Ex ((x. 0 : ( ( ) ( ext-real natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(All ((x. 4 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,(H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) <=> ((x. 4 : ( ( ) ( ext-real non empty natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) '=' (x. 0 : ( ( ) ( ext-real natural V14() V32() V33() V34() V35() V36() V37() ) Element of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real natural V14() ) Element of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) FinSequence of K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
for u being ( ( ) ( ) Element of E : ( ( non empty ) ( non empty ) set ) ) holds (def_func' (H : ( ( ZF-formula-like ) ( Relation-like K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -defined K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like FinSequence-like ZF-formula-like ) ZF-formula) ,f : ( ( Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29( VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of VAR : ( ( ) ( non empty V32() V33() V34() V35() V36() V37() ) Element of bool K45() : ( ( ) ( V32() V33() V34() V35() V36() V37() V38() ) Element of bool K41() : ( ( ) ( V32() V33() V34() V38() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,b1 : ( ( non empty ) ( non empty ) set ) ) )) : ( ( Function-like V29(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like V29(b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) ) .: u : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) in E : ( ( non empty ) ( non empty ) set ) ) holds
E : ( ( non empty ) ( non empty ) set ) is being_a_model_of_ZF ;