let Y be non empty set ; :: thesis: for a being Function of Y,BOOLEAN holds B_SUP (a,(%O Y)) = B_SUP a
let a be Function of Y,BOOLEAN; :: thesis: B_SUP (a,(%O Y)) = B_SUP a
let y be Element of Y; :: according to FUNCT_2:def 8 :: thesis: (B_SUP (a,(%O Y))) . y = (B_SUP a) . y
EqClass (y,(%O Y)) in %O Y ;
then EqClass (y,(%O Y)) in {Y} by PARTIT1:def 8;
then A1: EqClass (y,(%O Y)) = Y by TARSKI:def 1;

A2: now :: thesis: ( ( for x being Element of Y holds
( not x in EqClass (y,(%O Y)) or not a . x = TRUE ) ) & ( for x being Element of Y holds a . x = FALSE ) implies (B_SUP (a,(%O Y))) . y = (B_SUP a) . y )

assume that
A3: for x being Element of Y holds
( not x in EqClass (y,(%O Y)) or not a . x = TRUE ) and
A4: for x being Element of Y holds a . x = FALSE ; :: thesis: (B_SUP (a,(%O Y))) . y = (B_SUP a) . y
B_SUP a = O_el Y by A4, Def14;
then (B_SUP a) . y = FALSE by Def10;
hence (B_SUP (a,(%O Y))) . y = (B_SUP a) . y by A3, Def17; :: thesis: verum

end;

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

assume that
A5: ex x being Element of Y st
( x in EqClass (y,(%O Y)) & a . x = TRUE ) and
not for x being Element of Y holds a . x = FALSE ; :: thesis: (B_SUP (a,(%O Y))) . y = (B_SUP a) . y
B_SUP a = I_el Y by A5, Def14;
then (B_SUP a) . y = TRUE by Def11;
hence (B_SUP (a,(%O Y))) . y = (B_SUP a) . y by A5, Def17; :: thesis: verum

end;

hence (B_SUP (a,(%O Y))) . y = (B_SUP a) . y by A2, A1, XBOOLEAN:def 3; :: thesis: verum