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
A1: 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 A2: 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 A2; :: thesis: verum
end;
A3: 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
A4: not for x being Element of Y holds a . x = TRUE and
A5: 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 A4, Def13;
then (B_INF a) . y = FALSE by Def10;
hence (B_INF (a,(%O Y))) . y = (B_INF a) . y by A5, 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
A6: for x being Element of Y holds a . x = TRUE and
A7: 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 A6, Def13;
then (B_INF a) . y = TRUE by Def11;
hence (B_INF (a,(%O Y))) . y = (B_INF a) . y by A7, Def16; :: thesis: verum
end;
hence (B_INF (a,(%O Y))) . y = (B_INF a) . y by A1, A3; :: thesis: verum