let Y be non empty set ; :: thesis: for a being Element of Funcs Y,BOOLEAN holds B_INF a,(%O Y) = B_INF a
let a be Element of Funcs Y,BOOLEAN ; :: thesis: B_INF a,(%O Y) = B_INF a
consider k3 being Function such that
A1: B_INF a,(%O Y) = k3 and
A2: dom k3 = Y and
rng k3 c= BOOLEAN by FUNCT_2:def 2;
consider k4 being Function such that
A3: B_INF a = k4 and
A4: dom k4 = Y and
rng k4 c= BOOLEAN by FUNCT_2:def 2;
for y being Element of Y holds (B_INF a,(%O Y)) . y = (B_INF a) . y

proof

let y be Element of Y; :: thesis: (B_INF a,(%O Y)) . y = (B_INF a) . y

A5: now

EqClass y,(%O Y) in %O Y ;
then EqClass y,(%O Y) in {Y} by PARTIT1:def 9;
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

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, Def16;
then (B_INF a) . y = FALSE by Def13;
hence (B_INF a,(%O Y)) . y = (B_INF a) . y by A9, Def19; :: thesis: verum

end;

now

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, Def16;
then (B_INF a) . y = TRUE by Def14;
hence (B_INF a,(%O Y)) . y = (B_INF a) . y by A11, Def19; :: thesis: verum

end;

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

end;

then for u being set st u in Y holds
k3 . u = k4 . u by A1, A3;
hence B_INF a,(%O Y) = B_INF a by A1, A2, A3, A4, FUNCT_1:9; :: thesis: verum