let Y be non empty set ; :: thesis: for a, b being Function of 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 Function of 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))
let y be Element of Y; :: according to FUNCT_2:def 8 :: thesis: (B_INF ((a '&' b),PA)) . y = ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y

A1: now :: thesis: ( ( 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 ) implies (B_INF ((a '&' b),PA)) . y = ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y )

assume that
for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE and
A2: 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
(B_INF (b,PA)) . y = FALSE by A2, Def16;
then ((B_INF (a,PA)) . y) '&' ((B_INF (b,PA)) . y) = FALSE ;
then A3: ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y = FALSE by MARGREL1:def 20;
consider x1 being Element of Y such that
A4: x1 in EqClass (y,PA) and
A5: b . x1 <> TRUE by A2;
b . x1 = FALSE by A5, XBOOLEAN:def 3;
then (a . x1) '&' (b . x1) = FALSE ;
then (a '&' b) . x1 <> TRUE by MARGREL1:def 20;
hence (B_INF ((a '&' b),PA)) . y = ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y by A4, A3, Def16; :: thesis: verum

end;

A6: now :: thesis: ( 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 ) implies (B_INF ((a '&' b),PA)) . y = ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y )

assume that
A7: ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) and
A8: 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
(B_INF (b,PA)) . y = FALSE by A8, Def16;
then ((B_INF (a,PA)) . y) '&' ((B_INF (b,PA)) . y) = FALSE ;
then A9: ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y = FALSE by MARGREL1:def 20;
consider xa being Element of Y such that
A10: xa in EqClass (y,PA) and
A11: a . xa <> TRUE by A7;
a . xa = FALSE by A11, XBOOLEAN:def 3;
then (a . xa) '&' (b . xa) = FALSE ;
then (a '&' b) . xa <> TRUE by MARGREL1:def 20;
hence (B_INF ((a '&' b),PA)) . y = ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y by A10, A9, Def16; :: thesis: verum

end;

A12: now :: thesis: ( ( 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 ) implies (B_INF ((a '&' b),PA)) . y = ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y )

assume that
A13: for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE and
A14: 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
A15: 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 A16: x in EqClass (y,PA) ; :: thesis: (a '&' b) . x = TRUE
then b . x = TRUE by A14;
then (a . x) '&' (b . x) = TRUE '&' TRUE by A13, A16;
hence (a '&' b) . x = TRUE by MARGREL1:def 20; :: thesis: verum

end;

(B_INF (b,PA)) . y = TRUE by A14, Def16;
then ((B_INF (a,PA)) . y) '&' ((B_INF (b,PA)) . y) = TRUE '&' TRUE by A13, Def16;
then ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y = TRUE by MARGREL1:def 20;
hence (B_INF ((a '&' b),PA)) . y = ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y by A15, Def16; :: thesis: verum

end;

now :: thesis: ( 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 ) implies (B_INF ((a '&' b),PA)) . y = ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y )

assume that
A17: ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) and
A18: 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
(B_INF (b,PA)) . y = TRUE by A18, Def16;
then ((B_INF (a,PA)) . y) '&' ((B_INF (b,PA)) . y) = FALSE '&' TRUE by A17, Def16;
then A19: ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y = FALSE by MARGREL1:def 20;
consider x1 being Element of Y such that
A20: x1 in EqClass (y,PA) and
A21: a . x1 <> TRUE by A17;
a . x1 = FALSE by A21, XBOOLEAN:def 3;
then (a . x1) '&' (b . x1) = FALSE ;
then (a '&' b) . x1 <> TRUE by MARGREL1:def 20;
hence (B_INF ((a '&' b),PA)) . y = ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y by A20, A19, Def16; :: thesis: verum

end;

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