let Y be non empty set ; :: thesis: for a, b being Function of 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 Function of 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))
let y be Element of Y; :: according to FUNCT_2:def 8 :: thesis: (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y
A1: now :: thesis: ( ex x being Element of Y st
( x in EqClass (y,PA) & (a 'or' b) . x = TRUE ) implies (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y )
assume A2: 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
A3: x1 in EqClass (y,PA) and
A4: (a 'or' b) . x1 = TRUE ;
A5: ( ( 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;
A6: (a . x1) 'or' (b . x1) = TRUE by A4, Def4;
now :: thesis: ( ( a . x1 = FALSE & b . x1 = TRUE & (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y ) or ( a . x1 = TRUE & b . x1 = FALSE & (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y ) or ( a . x1 = TRUE & b . x1 = TRUE & (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y ) )
per cases ( ( a . x1 = FALSE & b . x1 = TRUE ) or ( a . x1 = TRUE & b . x1 = FALSE ) or ( a . x1 = TRUE & b . x1 = TRUE ) ) by A6, A5;
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 A3, Def17;
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 Def4;
hence (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y by A2, Def17; :: 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 A3, Def17;
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 Def4;
hence (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y by A2, Def17; :: 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 A3, Def17;
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 Def4;
hence (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y by A2, Def17; :: 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 :: thesis: ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not (a 'or' b) . x = TRUE ) ) implies (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y )
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
now :: thesis: for x being Element of Y holds
( not x in EqClass (y,PA) or not b . x = TRUE )
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
A8: x1 in EqClass (y,PA) and
A9: b . x1 = TRUE ;
(a . x1) 'or' (b . x1) = TRUE by A9;
then (a 'or' b) . x1 = TRUE by Def4;
hence contradiction by A7, A8; :: thesis: verum
end;
then A10: (B_SUP (b,PA)) . y = FALSE by Def17;
now :: thesis: for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE )
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
A11: x1 in EqClass (y,PA) and
A12: a . x1 = TRUE ;
(a . x1) 'or' (b . x1) = TRUE by A12;
then (a 'or' b) . x1 = TRUE by Def4;
hence contradiction by A7, A11; :: thesis: verum
end;
then ((B_SUP (a,PA)) . y) 'or' ((B_SUP (b,PA)) . y) = FALSE 'or' FALSE by A10, Def17;
then ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y = FALSE by Def4;
hence (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y by A7, Def17; :: thesis: verum
end;
hence (B_SUP ((a 'or' b),PA)) . y = ((B_SUP (a,PA)) 'or' (B_SUP (b,PA))) . y by A1; :: thesis: verum