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_SUP ((a 'or' b),PA) = (B_SUP (a,PA)) 'or' (B_SUP (b,PA))
let a, b be Element of Funcs (Y,BOOLEAN); :: thesis: for PA being a_partition of Y holds B_SUP ((a 'or' b),PA) = (B_SUP (a,PA)) 'or' (B_SUP (b,PA))
let PA be a_partition of Y; :: thesis: B_SUP ((a 'or' b),PA) = (B_SUP (a,PA)) 'or' (B_SUP (b,PA))
consider k3 being Function such that
A1: B_SUP ((a 'or' b),PA) = k3 and
A2: dom k3 = Y and
rng k3 c= BOOLEAN by FUNCT_2:def 2;
consider k4 being Function such that
A3: (B_SUP (a,PA)) 'or' (B_SUP (b,PA)) = k4 and
A4: dom k4 = Y and
rng k4 c= BOOLEAN by FUNCT_2:def 2;
for y being Element of Y holds (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y

proof

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

A5: now

assume A6: ex x being Element of Y st
( x in EqClass (y,PA) & (a 'or' b) . x = TRUE ) ; :: thesis: (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y
then consider x1 being Element of Y such that
A7: x1 in EqClass (y,PA) and
A8: (a 'or' b) . x1 = TRUE ;
A9: ( ( a . x1 = FALSE & b . x1 = FALSE ) or ( a . x1 = FALSE & b . x1 = TRUE ) or ( a . x1 = TRUE & b . x1 = FALSE ) or ( a . x1 = TRUE & b . x1 = TRUE ) ) by XBOOLEAN:def 3;
A10: (a . x1) 'or' (b . x1) = TRUE by A8, Def7;

now

per cases ( ( a . x1 = FALSE & b . x1 = TRUE ) or ( a . x1 = TRUE & b . x1 = FALSE ) or ( a . x1 = TRUE & b . x1 = TRUE ) ) by A10, A9;

case ( a . x1 = FALSE & b . x1 = TRUE ) ; :: thesis: (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y

then (B_SUP (b,PA)) . y = TRUE by A7, Def20;
then ((B_SUP (a,PA)) . y) 'or' ((B_SUP (b,PA)) . y) = TRUE ;
then ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y = TRUE by Def7;
hence (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y by A6, Def20; :: thesis: verum

end;

case ( a . x1 = TRUE & b . x1 = FALSE ) ; :: thesis: (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y

then (B_SUP (a,PA)) . y = TRUE by A7, Def20;
then ((B_SUP (a,PA)) . y) 'or' ((B_SUP (b,PA)) . y) = TRUE ;
then ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y = TRUE by Def7;
hence (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y by A6, Def20; :: thesis: verum

end;

case ( a . x1 = TRUE & b . x1 = TRUE ) ; :: thesis: (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y

then (B_SUP (b,PA)) . y = TRUE by A7, Def20;
then ((B_SUP (a,PA)) . y) 'or' ((B_SUP (b,PA)) . y) = TRUE ;
then ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y = TRUE by Def7;
hence (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y by A6, Def20; :: thesis: verum

end;

end;

end;

hence (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y ; :: thesis: verum

end;

now

assume A11: for x being Element of Y holds
( not x in EqClass (y,PA) or not (a 'or' b) . x = TRUE ) ; :: thesis: (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y

now

assume ex x being Element of Y st
( x in EqClass (y,PA) & b . x = TRUE ) ; :: thesis: contradiction
then consider x1 being Element of Y such that
A12: x1 in EqClass (y,PA) and
A13: b . x1 = TRUE ;
(a . x1) 'or' (b . x1) = TRUE by A13;
then (a 'or' b) . x1 = TRUE by Def7;
hence contradiction by A11, A12; :: thesis: verum

end;

then A14: (B_SUP (b,PA)) . y = FALSE by Def20;

now

assume ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) ; :: thesis: contradiction
then consider x1 being Element of Y such that
A15: x1 in EqClass (y,PA) and
A16: a . x1 = TRUE ;
(a . x1) 'or' (b . x1) = TRUE by A16;
then (a 'or' b) . x1 = TRUE by Def7;
hence contradiction by A11, A15; :: thesis: verum

end;

then ((B_SUP (a,PA)) . y) 'or' ((B_SUP (b,PA)) . y) = FALSE 'or' FALSE by A14, Def20;
then ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y = FALSE by Def7;
hence (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y by A11, Def20; :: thesis: verum

end;

hence (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y by A5; :: thesis: verum

end;

then for u being set st u in Y holds
k3 . u = k4 . u by A1, A3;
hence B_SUP ((a 'or' b),PA) = (B_SUP (a,PA)) 'or' (B_SUP (b,PA)) by A1, A2, A3, A4, FUNCT_1:2; :: thesis: verum