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

A5: 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
A6: 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 A6, Def16;
then ((B_INF (a,PA)) . y) '&' ((B_INF (b,PA)) . y) = FALSE ;
then A7: ((B_INF (a,PA)) '&' (B_INF (b,PA))) . y = FALSE by MARGREL1:def 20;
consider x1 being Element of Y such that
A8: x1 in EqClass (y,PA) and
A9: b . x1 <> TRUE by A6;
b . x1 = FALSE by A9, 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 A8, A7, Def16; :: thesis: verum

end;

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

end;

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

end;

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

end;

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