:: BVFUNC_2 semantic presentation

begin

definition
let X be ( ( ) ( ) set ) ;
:: original: PARTITIONS
redefine func PARTITIONS X -> ( ( partition-membered ) ( partition-membered ) Part-Family of X : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) ;
end;

definition
let X be ( ( ) ( ) set ) ;
let F be ( ( non empty partition-membered ) ( non empty partition-membered ) Part-Family of X : ( ( ) ( ) set ) ) ;
:: original: Element
redefine mode Element of F -> ( ( ) ( with_non-empty_elements ) a_partition of X : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) ;
end;

theorem :: BVFUNC_2:1
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for y being ( ( ) ( ) Element of Y : ( ( non empty ) ( non empty ) set ) ) ex X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st
( y : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) in X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & ex h being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ex F being ( ( ) ( ) Subset-Family of ) st
( dom h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & rng h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = F : ( ( ) ( ) Subset-Family of ) & ( for d being ( ( ) ( ) set ) st d : ( ( ) ( ) set ) in G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . d : ( ( ) ( ) set ) : ( ( ) ( ) set ) in d : ( ( ) ( ) set ) ) & X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) = Intersect F : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) <> {} : ( ( ) ( empty V55() ) set ) ) ) ;

definition
let Y be ( ( non empty ) ( non empty ) set ) ;
let G be ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
func '/\' G -> ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) means :: BVFUNC_2:def 1
 for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in it : ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) iff ex h being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ex F being ( ( ) ( ) Subset-Family of ) st
( dom h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = G : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) & rng h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = F : ( ( ) ( ) Subset-Family of ) & ( for d being ( ( ) ( ) set ) st d : ( ( ) ( ) set ) in G : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) holds
h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . d : ( ( ) ( ) set ) : ( ( ) ( ) set ) in d : ( ( ) ( ) set ) ) & x : ( ( ) ( ) set ) = Intersect F : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) set ) <> {} : ( ( ) ( empty V55() ) set ) ) );
end;

definition
let Y be ( ( non empty ) ( non empty ) set ) ;
let G be ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
let b be ( ( ) ( ) set ) ;
pred b is_upper_min_depend_of G means :: BVFUNC_2:def 2
( ( for d being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) st d : ( ( ) ( ) set ) in G : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) holds
b : ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) is_a_dependent_set_of d : ( ( ) ( ) set ) ) & ( for e being ( ( ) ( ) set ) st e : ( ( ) ( ) set ) c= b : ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) & ( for d being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) st d : ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) in G : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) holds
e : ( ( ) ( ) set ) is_a_dependent_set_of d : ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) ) holds
e : ( ( ) ( ) set ) = b : ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) ) );
end;

theorem :: BVFUNC_2:2
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for y being ( ( ) ( ) Element of Y : ( ( non empty ) ( non empty ) set ) ) st G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) <> {} : ( ( ) ( empty V55() ) set ) holds
ex X being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st
( y : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) in X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) & X : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) is_upper_min_depend_of G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) ;

definition
let Y be ( ( non empty ) ( non empty ) set ) ;
let G be ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
func '\/' G -> ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) means :: BVFUNC_2:def 3
 for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in it : ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) iff x : ( ( ) ( ) set ) is_upper_min_depend_of G : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) if G : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) <> {} : ( ( ) ( empty V55() ) set )
otherwise it : ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) = %I Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( with_non-empty_elements ) a_partition of Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) ;
end;

theorem :: BVFUNC_2:3
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) in G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) '>' '/\' G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:4
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) in G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) '<' '\/' G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ;

begin

definition
let Y be ( ( non empty ) ( non empty ) set ) ;
let G be ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
attr G is generating means :: BVFUNC_2:def 4
 '/\' G : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) = %I Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( with_non-empty_elements ) a_partition of Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) ;
end;

definition
let Y be ( ( non empty ) ( non empty ) set ) ;
let G be ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
attr G is independent means :: BVFUNC_2:def 5
 for h being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function)
for F being ( ( ) ( ) Subset-Family of ) st dom h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = G : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) & rng h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = F : ( ( ) ( ) Subset-Family of ) & ( for d being ( ( ) ( ) set ) st d : ( ( ) ( ) set ) in G : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) holds
h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . d : ( ( ) ( ) set ) : ( ( ) ( ) set ) in d : ( ( ) ( ) set ) ) holds
Intersect F : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) <> {} : ( ( ) ( empty V55() ) set ) ;
end;

definition
let Y be ( ( non empty ) ( non empty ) set ) ;
let G be ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
pred G is_a_coordinate means :: BVFUNC_2:def 6
( G : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) is independent & G : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) is generating );
end;

definition
let Y be ( ( non empty ) ( non empty ) set ) ;
let PA be ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) ;
:: original: {
redefine func {PA} -> ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
end;

definition
let Y be ( ( non empty ) ( non empty ) set ) ;
let PA be ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) ;
let G be ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
func CompF (PA,G) -> ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) equals :: BVFUNC_2:def 7
 '/\' (G : ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) \ {PA : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool (PARTITIONS Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( partition-membered ) ( non empty partition-membered ) Part-Family of Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) ;
end;

definition
let Y be ( ( non empty ) ( non empty ) set ) ;
let a be ( ( Function-like quasi_total ) ( Relation-like Y : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ;
let G be ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
let PA be ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) ;
pred a is_independent_of PA,G means :: BVFUNC_2:def 8
a : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) is_dependent_of CompF (PA : ( ( ) ( ) set ) ,G : ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) ;
end;

definition
let Y be ( ( non empty ) ( non empty ) set ) ;
let a be ( ( Function-like quasi_total ) ( Relation-like Y : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ;
let G be ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
let PA be ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) ;
func All (a,PA,G) -> ( ( Function-like quasi_total ) ( Relation-like Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) , BOOLEAN : ( ( ) ( non empty ) set ) ) equals :: BVFUNC_2:def 9
 B_INF (a : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ,(CompF (PA : ( ( ) ( ) set ) ,G : ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) ) : ( ( Function-like quasi_total ) ( Relation-like Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let Y be ( ( non empty ) ( non empty ) set ) ;
let a be ( ( Function-like quasi_total ) ( Relation-like Y : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ;
let G be ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;
let PA be ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) ;
func Ex (a,PA,G) -> ( ( Function-like quasi_total ) ( Relation-like Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) , BOOLEAN : ( ( ) ( non empty ) set ) ) equals :: BVFUNC_2:def 10
 B_SUP (a : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ,(CompF (PA : ( ( ) ( ) set ) ,G : ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ) ) : ( ( Function-like quasi_total ) ( Relation-like Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:Y : ( ( ) ( V39() boolean ) Element of BOOLEAN : ( ( ) ( non empty ) set ) ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: BVFUNC_2:5
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds All (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) is_dependent_of CompF (PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:6
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds Ex (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) is_dependent_of CompF (PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:7
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds All ((I_el Y : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:8
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds Ex ((I_el Y : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:9
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds All ((O_el Y : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) = O_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:10
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds Ex ((O_el Y : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) = O_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:11
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds All (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '<' a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:12
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '<' Ex (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:13
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for a, b being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds (All (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' (All (b : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) '<' All ((a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:14
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for a, b being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds All ((a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '<' (All (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' (All (b : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:15
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds Ex ((a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '<' (Ex (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' (Ex (b : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:16
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for a, b being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds (Ex (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'xor' (Ex (b : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) '<' Ex ((a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'xor' b : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:17
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for a, b being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds (Ex (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' (Ex (b : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) '<' Ex ((a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:18
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds 'not' (All (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = Ex (('not' a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:19
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds 'not' (Ex (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = All (('not' a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:20
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for u, a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) is_independent_of PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
All ((u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) = u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' (All (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:21
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for u, a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) is_independent_of PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
All ((a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) = (Ex (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:22
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for u, a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) is_independent_of PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
All ((u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) = u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' (All (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:23
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for u, a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) is_independent_of PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
All ((a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) = (All (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:24
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for u, a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) is_independent_of PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
All ((a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '<' (Ex (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:25
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for u, a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) is_independent_of PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
All ((u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) = u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' (All (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:26
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for u, a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) is_independent_of PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
All ((a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) = (All (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:27
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for a, u being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds All ((a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '<' (Ex (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:28
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for u, a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) is_independent_of PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
All ((u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'xor' a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '<' u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'xor' (All (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:29
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for u, a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) is_independent_of PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
All ((a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'xor' u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '<' (All (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'xor' u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:30
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for u, a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) is_independent_of PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
All ((u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '<' u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' (All (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:31
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for u, a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) is_independent_of PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
All ((a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '<' (All (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:32
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for u, a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) is_independent_of PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
Ex ((u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) = u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' (Ex (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:33
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for u, a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) is_independent_of PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
Ex ((a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) = (Ex (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:34
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for u, a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) is_independent_of PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
Ex ((u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) = u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' (Ex (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:35
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for u, a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) is_independent_of PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
Ex ((a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) = (Ex (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:36
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for u, a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' (Ex (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) '<' Ex ((u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:37
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for a, u being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds (Ex (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) '<' Ex ((a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:38
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for u, a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) is_independent_of PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'xor' (Ex (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) '<' Ex ((u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'xor' a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_2:39
for Y being ( ( non empty ) ( non empty ) set )
for G being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) )
for u, a being ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for PA being ( ( ) ( non empty with_non-empty_elements ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) is_independent_of PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
(Ex (a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'xor' u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) '<' Ex ((a : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'xor' u : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( non empty with_non-empty_elements ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined BOOLEAN : ( ( ) ( non empty ) set ) -valued Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ;