let Y be non empty set ; :: thesis: for a being Function of Y,BOOLEAN holds B_INF (a,(%O Y)) = B_INF a
let a be Function of Y,BOOLEAN; :: thesis: B_INF (a,(%O Y)) = B_INF a
let y be Element of Y; :: according to FUNCT_2:def 8 :: thesis: (B_INF (a,(%O Y))) . y = (B_INF a) . y

A5: now :: thesis: ( not for x being Element of Y holds a . x = TRUE implies ex x being Element of Y st
( x in EqClass (y,(%O Y)) & not a . x = TRUE ) )

EqClass (y,(%O Y)) in %O Y ;
then EqClass (y,(%O Y)) in {Y} by PARTIT1:def 8;
then A6: EqClass (y,(%O Y)) = Y by TARSKI:def 1;
assume ( not for x being Element of Y holds a . x = TRUE & ( for x being Element of Y st x in EqClass (y,(%O Y)) holds
a . x = TRUE ) ) ; :: thesis: contradiction
hence contradiction by A6; :: thesis: verum

end;

A7: now :: thesis: ( not for x being Element of Y holds a . x = TRUE & ex x being Element of Y st
( x in EqClass (y,(%O Y)) & not a . x = TRUE ) implies (B_INF (a,(%O Y))) . y = (B_INF a) . y )

assume that
A8: not for x being Element of Y holds a . x = TRUE and
A9: ex x being Element of Y st
( x in EqClass (y,(%O Y)) & not a . x = TRUE ) ; :: thesis: (B_INF (a,(%O Y))) . y = (B_INF a) . y
B_INF a = O_el Y by A8, Def13;
then (B_INF a) . y = FALSE by Def10;
hence (B_INF (a,(%O Y))) . y = (B_INF a) . y by A9, Def16; :: thesis: verum

end;

now :: thesis: ( ( for x being Element of Y holds a . x = TRUE ) & ( for x being Element of Y st x in EqClass (y,(%O Y)) holds
a . x = TRUE ) implies (B_INF (a,(%O Y))) . y = (B_INF a) . y )

assume that
A10: for x being Element of Y holds a . x = TRUE and
A11: for x being Element of Y st x in EqClass (y,(%O Y)) holds
a . x = TRUE ; :: thesis: (B_INF (a,(%O Y))) . y = (B_INF a) . y
B_INF a = I_el Y by A10, Def13;
then (B_INF a) . y = TRUE by Def11;
hence (B_INF (a,(%O Y))) . y = (B_INF a) . y by A11, Def16; :: thesis: verum

end;

hence (B_INF (a,(%O Y))) . y = (B_INF a) . y by A5, A7; :: thesis: verum