let Y be non empty set ; :: thesis: for a being Element of Funcs Y,BOOLEAN holds B_SUP a,(%O Y) = B_SUP a
let a be Element of Funcs Y,BOOLEAN ; :: thesis: B_SUP a,(%O Y) = B_SUP a
A1: for y being Element of Y holds (B_SUP a,(%O Y)) . y = (B_SUP a) . y

proof

let y be Element of Y; :: 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 9;
then A2: EqClass y,(%O Y) = Y by TARSKI:def 1;

A3: now

assume A4: ( 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 ) ; :: thesis: (B_SUP a,(%O Y)) . y = (B_SUP a) . y
then B_SUP a = I_el Y by Def17;
then (B_SUP a) . y = TRUE by Def14;
hence (B_SUP a,(%O Y)) . y = (B_SUP a) . y by A4, Def20; :: thesis: verum

end;

A5: now

assume A6: ( ( 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 ) ) ; :: thesis: (B_SUP a,(%O Y)) . y = (B_SUP a) . y
then B_SUP a = O_el Y by Def17;
then (B_SUP a) . y = FALSE by Def13;
hence (B_SUP a,(%O Y)) . y = (B_SUP a) . y by A6, Def20; :: thesis: verum

end;

now

assume A7: ( ( for x being Element of Y holds
( not x in EqClass y,(%O Y) or not a . x = TRUE ) ) & not for x being Element of Y holds a . x = FALSE ) ; :: thesis: contradiction
then consider x1 being Element of Y such that
A8: a . x1 <> FALSE ;
( x1 in Y & a . x1 = TRUE ) by A8, XBOOLEAN:def 3;
hence contradiction by A2, A7; :: thesis: verum

end;

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

end;

consider k3 being Function such that
A9: ( B_SUP a,(%O Y) = k3 & dom k3 = Y & rng k3 c= BOOLEAN ) by FUNCT_2:def 2;
consider k4 being Function such that
A10: ( B_SUP a = k4 & dom k4 = Y & rng k4 c= BOOLEAN ) by FUNCT_2:def 2;
for u being set st u in Y holds
k3 . u = k4 . u by A1, A9, A10;
hence B_SUP a,(%O Y) = B_SUP a by A9, A10, FUNCT_1:9; :: thesis: verum