:: BVFUNC_4 semantic presentation

begin

theorem :: BVFUNC_4:1
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) st a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '<' b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' c : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_4:2
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c being ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) st a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' c : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds
a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '<' b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_4:3
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_4:4
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_4:5
for Y being ( ( non empty ) ( non empty ) set )
for a being ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' ('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = O_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_4:6
for Y being ( ( non empty ) ( non empty ) set )
for a being ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' ('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_4:7
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_4:8
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = ('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_4:9
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'xor' b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = (('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' ('not' b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_4:10
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) holds
( a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) iff ( a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: BVFUNC_4:11
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) st a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
('not' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'eqv' ('not' b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_4:12
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c, d being ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) st a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & c : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' d : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
(a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' c : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'eqv' (b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' d : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_4:13
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c, d being ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) st a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & c : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' d : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
(a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' c : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'eqv' (b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' d : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_4:14
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c, d being ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) st a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & c : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' d : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
(a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' c : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'eqv' (b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'or' d : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_4:15
for Y being ( ( non empty ) ( non empty ) set )
for a, b, c, d being ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) st a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & c : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' d : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
(a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' c : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'eqv' (b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' d : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

begin

theorem :: BVFUNC_4:16
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds All ((a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = (All ((a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (All ((b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_4:17
for Y being ( ( non empty ) ( non empty ) set )
for a being ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for PA, PB being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PB : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_4:18
for Y being ( ( non empty ) ( non empty ) set )
for a, u being ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' u : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
(All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' u : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_4:19
for Y being ( ( non empty ) ( non empty ) set )
for u being ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st u : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) is_independent_of PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) holds
Ex (u : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' u : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ;

theorem :: BVFUNC_4:20
for Y being ( ( non empty ) ( non empty ) set )
for u being ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st u : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) is_independent_of PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) holds
u : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '<' All (u : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_4:21
for Y being ( ( non empty ) ( non empty ) set )
for u being ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for PA, PB being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st u : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) is_independent_of PB : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) holds
All (u : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' All (u : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PB : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_4:22
for Y being ( ( non empty ) ( non empty ) set )
for u being ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for PA, PB being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st u : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) is_independent_of PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) holds
Ex (u : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' Ex (u : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PB : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_4:23
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds All ((a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' (All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'eqv' (All (b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_4:24
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds All ((a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) '&' (All (b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_4:25
for Y being ( ( non empty ) ( non empty ) set )
for a, u being ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) holds (All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' u : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '<' Ex ((a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'imp' u : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_4:26
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
(All (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'eqv' (All (b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_4:27
for Y being ( ( non empty ) ( non empty ) set )
for a, b being ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of Y : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) )
for G being ( ( ) ( ) Subset of ( ( ) ( ) set ) )
for PA being ( ( ) ( ) a_partition of Y : ( ( non empty ) ( non empty ) set ) ) st a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) 'eqv' b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
(Ex (a : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'eqv' (Ex (b : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) , BOOLEAN : ( ( ) ( non empty ) set ) ) ,PA : ( ( ) ( ) a_partition of b1 : ( ( non empty ) ( non empty ) set ) ) ,G : ( ( ) ( ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = I_el Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;