:: BVFUNC_8 semantic presentation

begin

theorem :: BVFUNC_8:1
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 ) ) 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 ) ) '&' 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(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 K10(K11(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' 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(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' 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_8:2
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 ) ) 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 ) ) '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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(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 K10(K11(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 ) ) '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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(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 ) ) '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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_8:3
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 ) ) 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 K10(K11(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 ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) 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 K10(K11(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' 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 K10(K11(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 ) ) '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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) 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 ) ) '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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_8:4
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 ) ) 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' 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) 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 K10(K11(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' 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 K10(K11(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' 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(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 ) ) '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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_8:5
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 ) ) 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 K10(K11(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' 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(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 ) ) '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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(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 K10(K11(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' 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(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 ) ) '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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(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' 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_8:6
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 ) ) '&' 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 K10(K11(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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_8: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 ) ) = (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 K10(K11(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 ) ) 'or' ('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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_8:8
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 ) ) 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 ) ) '&' 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 K10(K11(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 ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(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 ) ) '&' 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' ('not' 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(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 ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' ('not' 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_8:9
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 ) ) 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) 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 K10(K11(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 ) ) '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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' ('not' 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(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 ) ) 'or' ('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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(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 ) ) 'or' ('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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' ('not' 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_8: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 ) ) '&' 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 K10(K11(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 ) ) '&' (('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 K10(K11(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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_8: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 ) ) 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' 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 K10(K11(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 ) ) '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 K10(K11(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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_8:12
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 K10(K11(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 ) ) '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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_8:13
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 K10(K11(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 ) ) '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 K10(K11(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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' ('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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_8:14
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 ) ) 'xor' (I_el Y : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_8:15
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 ) ) 'xor' (O_el Y : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(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_8: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 ) ) 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 K10(K11(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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'xor' ('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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_8:17
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 'not' (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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(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 ) ) 'xor' ('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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_8:18
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 K10(K11(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 ) ) 'or' ('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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(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 K10(K11(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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_8:19
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 K10(K11(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 ) ) '&' 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_8:20
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 ) ) 'eqv' (I_el Y : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(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_8:21
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 ) ) 'eqv' (O_el Y : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_8:22
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 'not' (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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(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 ) ) '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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_8: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 ) ) 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 K10(K11(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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'eqv' ('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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_8: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 ) ) 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 K10(K11(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 K10(K11(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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_8:25
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 K10(K11(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' 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'eqv' 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_8:26
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 ) ) 'imp' (('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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'eqv' ('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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_8: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 ) ) 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) 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 K10(K11(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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_8:28
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 ) ) 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 K10(K11(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' 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) '&' (('not' 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' ('not' 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'imp' (('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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) 'or' ('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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: BVFUNC_8:29
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 ) ) 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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) 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 ) ) 'imp' (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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) 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 ) ) '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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Function-like quasi_total boolean-valued ) Element of K10(K11(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 K10(K11(b1 : ( ( non empty ) ( non empty ) set ) ,BOOLEAN : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;