let Y be non empty set ; :: thesis: for a, b being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y holds B_INF (a '&' b),PA = (B_INF a,PA) '&' (B_INF b,PA)
let a, b be Element of Funcs Y,BOOLEAN ; :: thesis: for PA being a_partition of Y holds B_INF (a '&' b),PA = (B_INF a,PA) '&' (B_INF b,PA)
let PA be a_partition of Y; :: thesis: B_INF (a '&' b),PA = (B_INF a,PA) '&' (B_INF b,PA)
A1: for y being Element of Y holds (B_INF (a '&' b),PA) . y = ((B_INF a,PA) '&' (B_INF b,PA)) . y

proof

let y be Element of Y; :: thesis: (B_INF (a '&' b),PA) . y = ((B_INF a,PA) '&' (B_INF b,PA)) . y

A2: now

assume A3: ( ( for x being Element of Y st x in EqClass y,PA holds
a . x = TRUE ) & ( for x being Element of Y st x in EqClass y,PA holds
b . x = TRUE ) ) ; :: thesis: (B_INF (a '&' b),PA) . y = ((B_INF a,PA) '&' (B_INF b,PA)) . y
A4: for x being Element of Y st x in EqClass y,PA holds
(a '&' b) . x = TRUE

proof

let x be Element of Y; :: thesis: ( x in EqClass y,PA implies (a '&' b) . x = TRUE )
assume A5: x in EqClass y,PA ; :: thesis: (a '&' b) . x = TRUE
then b . x = TRUE by A3;
then (a . x) '&' (b . x) = TRUE '&' TRUE by A3, A5;
hence (a '&' b) . x = TRUE by MARGREL1:def 21; :: thesis: verum

end;

(B_INF b,PA) . y = TRUE by A3, Def19;
then ((B_INF a,PA) . y) '&' ((B_INF b,PA) . y) = TRUE '&' TRUE by A3, Def19;
then ((B_INF a,PA) '&' (B_INF b,PA)) . y = TRUE by MARGREL1:def 21;
hence (B_INF (a '&' b),PA) . y = ((B_INF a,PA) '&' (B_INF b,PA)) . y by A4, Def19; :: thesis: verum

end;

A6: now

assume A7: ( ( for x being Element of Y st x in EqClass y,PA holds
a . x = TRUE ) & ex x being Element of Y st
( x in EqClass y,PA & not b . x = TRUE ) ) ; :: thesis: (B_INF (a '&' b),PA) . y = ((B_INF a,PA) '&' (B_INF b,PA)) . y
then consider x1 being Element of Y such that
A8: ( x1 in EqClass y,PA & b . x1 <> TRUE ) ;
( x1 in EqClass y,PA & b . x1 = FALSE ) by A8, XBOOLEAN:def 3;
then (a . x1) '&' (b . x1) = FALSE ;
then A9: (a '&' b) . x1 <> TRUE by MARGREL1:def 21;
(B_INF b,PA) . y = FALSE by A7, Def19;
then ((B_INF a,PA) . y) '&' ((B_INF b,PA) . y) = FALSE ;
then ((B_INF a,PA) '&' (B_INF b,PA)) . y = FALSE by MARGREL1:def 21;
hence (B_INF (a '&' b),PA) . y = ((B_INF a,PA) '&' (B_INF b,PA)) . y by A8, A9, Def19; :: thesis: verum

end;

A10: now

assume A11: ( ex x being Element of Y st
( x in EqClass y,PA & not a . x = TRUE ) & ( for x being Element of Y st x in EqClass y,PA holds
b . x = TRUE ) ) ; :: thesis: (B_INF (a '&' b),PA) . y = ((B_INF a,PA) '&' (B_INF b,PA)) . y
then consider x1 being Element of Y such that
A12: ( x1 in EqClass y,PA & a . x1 <> TRUE ) ;
( x1 in EqClass y,PA & a . x1 = FALSE ) by A12, XBOOLEAN:def 3;
then (a . x1) '&' (b . x1) = FALSE ;
then A13: (a '&' b) . x1 <> TRUE by MARGREL1:def 21;
(B_INF b,PA) . y = TRUE by A11, Def19;
then ((B_INF a,PA) . y) '&' ((B_INF b,PA) . y) = FALSE '&' TRUE by A11, Def19;
then ((B_INF a,PA) '&' (B_INF b,PA)) . y = FALSE by MARGREL1:def 21;
hence (B_INF (a '&' b),PA) . y = ((B_INF a,PA) '&' (B_INF b,PA)) . y by A12, A13, Def19; :: thesis: verum

end;

now

assume A14: ( ex x being Element of Y st
( x in EqClass y,PA & not a . x = TRUE ) & ex x being Element of Y st
( x in EqClass y,PA & not b . x = TRUE ) ) ; :: thesis: (B_INF (a '&' b),PA) . y = ((B_INF a,PA) '&' (B_INF b,PA)) . y
then consider xa being Element of Y such that
A15: ( xa in EqClass y,PA & a . xa <> TRUE ) ;
( xa in EqClass y,PA & a . xa = FALSE ) by A15, XBOOLEAN:def 3;
then (a . xa) '&' (b . xa) = FALSE ;
then A16: (a '&' b) . xa <> TRUE by MARGREL1:def 21;
(B_INF b,PA) . y = FALSE by A14, Def19;
then ((B_INF a,PA) . y) '&' ((B_INF b,PA) . y) = FALSE ;
then ((B_INF a,PA) '&' (B_INF b,PA)) . y = FALSE by MARGREL1:def 21;
hence (B_INF (a '&' b),PA) . y = ((B_INF a,PA) '&' (B_INF b,PA)) . y by A15, A16, Def19; :: thesis: verum

end;

hence (B_INF (a '&' b),PA) . y = ((B_INF a,PA) '&' (B_INF b,PA)) . y by A2, A6, A10; :: thesis: verum

end;

consider k3 being Function such that
A17: ( B_INF (a '&' b),PA = k3 & dom k3 = Y & rng k3 c= BOOLEAN ) by FUNCT_2:def 2;
consider k4 being Function such that
A18: ( (B_INF a,PA) '&' (B_INF b,PA) = 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, A17, A18;
hence B_INF (a '&' b),PA = (B_INF a,PA) '&' (B_INF b,PA) by A17, A18, FUNCT_1:9; :: thesis: verum