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)
A1: 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

A2: now

assume A3: 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
A4: ( x1 in EqClass y,PA & (a 'or' b) . x1 = TRUE ) ;
A5: (a . x1) 'or' (b . x1) = TRUE by A4, Def7;
A6: ( ( 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;

now

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

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 A4, 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 A3, 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 A4, 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 A3, 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 A4, 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 A3, 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 A7: 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

A8: 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
A9: ( x1 in EqClass y,PA & a . x1 = TRUE ) ;
(a . x1) 'or' (b . x1) = TRUE by A9;
then (a 'or' b) . x1 = TRUE by Def7;
hence contradiction by A7, A9; :: thesis: verum

end;

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
A10: ( x1 in EqClass y,PA & b . x1 = TRUE ) ;
(a . x1) 'or' (b . x1) = TRUE by A10;
then (a 'or' b) . x1 = TRUE by Def7;
hence contradiction by A7, A10; :: thesis: verum

end;

then (B_SUP b,PA) . y = FALSE by Def20;
then ((B_SUP a,PA) . y) 'or' ((B_SUP b,PA) . y) = FALSE 'or' FALSE by A8, 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 A7, Def20; :: thesis: verum

end;

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

end;

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