let X, Y be non empty set ; for x, y being set
for E1, E2 being Subset of [:X,Y:] st E1 misses E2 holds
( (chi ((E1 \/ E2),[:X,Y:])) . (x,y) = ((chi ((X-section (E1,x)),Y)) . y) + ((chi ((X-section (E2,x)),Y)) . y) & (chi ((E1 \/ E2),[:X,Y:])) . (x,y) = ((chi ((Y-section (E1,y)),X)) . x) + ((chi ((Y-section (E2,y)),X)) . x) )
let x, y be set ; for E1, E2 being Subset of [:X,Y:] st E1 misses E2 holds
( (chi ((E1 \/ E2),[:X,Y:])) . (x,y) = ((chi ((X-section (E1,x)),Y)) . y) + ((chi ((X-section (E2,x)),Y)) . y) & (chi ((E1 \/ E2),[:X,Y:])) . (x,y) = ((chi ((Y-section (E1,y)),X)) . x) + ((chi ((Y-section (E2,y)),X)) . x) )
let E1, E2 be Subset of [:X,Y:]; ( E1 misses E2 implies ( (chi ((E1 \/ E2),[:X,Y:])) . (x,y) = ((chi ((X-section (E1,x)),Y)) . y) + ((chi ((X-section (E2,x)),Y)) . y) & (chi ((E1 \/ E2),[:X,Y:])) . (x,y) = ((chi ((Y-section (E1,y)),X)) . x) + ((chi ((Y-section (E2,y)),X)) . x) ) )
assume
E1 misses E2
; ( (chi ((E1 \/ E2),[:X,Y:])) . (x,y) = ((chi ((X-section (E1,x)),Y)) . y) + ((chi ((X-section (E2,x)),Y)) . y) & (chi ((E1 \/ E2),[:X,Y:])) . (x,y) = ((chi ((Y-section (E1,y)),X)) . x) + ((chi ((Y-section (E2,y)),X)) . x) )
then A1:
( X-section (E1,x) misses X-section (E2,x) & Y-section (E1,y) misses Y-section (E2,y) )
by Th29;
A2: (chi ((E1 \/ E2),[:X,Y:])) . (x,y) =
(chi ((X-section ((E1 \/ E2),x)),Y)) . y
by Th28
.=
(chi (((X-section (E1,x)) \/ (X-section (E2,x))),Y)) . y
by Th20
;
thus
(chi ((E1 \/ E2),[:X,Y:])) . (x,y) = ((chi ((X-section (E1,x)),Y)) . y) + ((chi ((X-section (E2,x)),Y)) . y)
(chi ((E1 \/ E2),[:X,Y:])) . (x,y) = ((chi ((Y-section (E1,y)),X)) . x) + ((chi ((Y-section (E2,y)),X)) . x)proof
per cases
( not y in Y or ( y in Y & y in (X-section (E1,x)) \/ (X-section (E2,x)) ) or ( y in Y & not y in (X-section (E1,x)) \/ (X-section (E2,x)) ) )
;
suppose B1:
not
y in Y
;
(chi ((E1 \/ E2),[:X,Y:])) . (x,y) = ((chi ((X-section (E1,x)),Y)) . y) + ((chi ((X-section (E2,x)),Y)) . y)
(
dom (chi (((X-section (E1,x)) \/ (X-section (E2,x))),Y)) = Y &
dom (chi ((X-section (E1,x)),Y)) = Y &
dom (chi ((X-section (E2,x)),Y)) = Y )
by FUNCT_3:def 3;
then
(
(chi ((E1 \/ E2),[:X,Y:])) . (
x,
y)
= 0 &
(chi ((X-section (E1,x)),Y)) . y = 0 &
(chi ((X-section (E2,x)),Y)) . y = 0 )
by A2, B1, FUNCT_1:def 2;
hence
(chi ((E1 \/ E2),[:X,Y:])) . (
x,
y)
= ((chi ((X-section (E1,x)),Y)) . y) + ((chi ((X-section (E2,x)),Y)) . y)
;
verum end; suppose A3:
(
y in Y &
y in (X-section (E1,x)) \/ (X-section (E2,x)) )
;
(chi ((E1 \/ E2),[:X,Y:])) . (x,y) = ((chi ((X-section (E1,x)),Y)) . y) + ((chi ((X-section (E2,x)),Y)) . y)then A4:
(chi ((E1 \/ E2),[:X,Y:])) . (
x,
y)
= 1
by A2, FUNCT_3:def 3;
per cases
( ( y in X-section (E1,x) & not y in X-section (E2,x) ) or ( not y in X-section (E1,x) & y in X-section (E2,x) ) )
by A1, A3, XBOOLE_0:5;
suppose
(
y in X-section (
E1,
x) & not
y in X-section (
E2,
x) )
;
(chi ((E1 \/ E2),[:X,Y:])) . (x,y) = ((chi ((X-section (E1,x)),Y)) . y) + ((chi ((X-section (E2,x)),Y)) . y)then
(
(chi ((X-section (E1,x)),Y)) . y = 1 &
(chi ((X-section (E2,x)),Y)) . y = 0 )
by FUNCT_3:def 3;
hence
(chi ((E1 \/ E2),[:X,Y:])) . (
x,
y)
= ((chi ((X-section (E1,x)),Y)) . y) + ((chi ((X-section (E2,x)),Y)) . y)
by A4, XXREAL_3:4;
verum end; suppose
( not
y in X-section (
E1,
x) &
y in X-section (
E2,
x) )
;
(chi ((E1 \/ E2),[:X,Y:])) . (x,y) = ((chi ((X-section (E1,x)),Y)) . y) + ((chi ((X-section (E2,x)),Y)) . y)then
(
(chi ((X-section (E1,x)),Y)) . y = 0 &
(chi ((X-section (E2,x)),Y)) . y = 1 )
by FUNCT_3:def 3;
hence
(chi ((E1 \/ E2),[:X,Y:])) . (
x,
y)
= ((chi ((X-section (E1,x)),Y)) . y) + ((chi ((X-section (E2,x)),Y)) . y)
by A4, XXREAL_3:4;
verum end; end; end; suppose A5:
(
y in Y & not
y in (X-section (E1,x)) \/ (X-section (E2,x)) )
;
(chi ((E1 \/ E2),[:X,Y:])) . (x,y) = ((chi ((X-section (E1,x)),Y)) . y) + ((chi ((X-section (E2,x)),Y)) . y)then A6:
(chi ((E1 \/ E2),[:X,Y:])) . (
x,
y)
= 0
by A2, FUNCT_3:def 3;
( not
y in X-section (
E1,
x) & not
y in X-section (
E2,
x) )
by A5, XBOOLE_0:def 3;
then
(
(chi ((X-section (E1,x)),Y)) . y = 0 &
(chi ((X-section (E2,x)),Y)) . y = 0 )
by A5, FUNCT_3:def 3;
hence
(chi ((E1 \/ E2),[:X,Y:])) . (
x,
y)
= ((chi ((X-section (E1,x)),Y)) . y) + ((chi ((X-section (E2,x)),Y)) . y)
by A6;
verum end; end;
end;
C2: (chi ((E1 \/ E2),[:X,Y:])) . (x,y) =
(chi ((Y-section ((E1 \/ E2),y)),X)) . x
by Th28
.=
(chi (((Y-section (E1,y)) \/ (Y-section (E2,y))),X)) . x
by Th20
;
per cases
( not x in X or ( x in X & x in (Y-section (E1,y)) \/ (Y-section (E2,y)) ) or ( x in X & not x in (Y-section (E1,y)) \/ (Y-section (E2,y)) ) )
;
suppose B1:
not
x in X
;
(chi ((E1 \/ E2),[:X,Y:])) . (x,y) = ((chi ((Y-section (E1,y)),X)) . x) + ((chi ((Y-section (E2,y)),X)) . x)
(
dom (chi (((Y-section (E1,y)) \/ (Y-section (E2,y))),X)) = X &
dom (chi ((Y-section (E1,y)),X)) = X &
dom (chi ((Y-section (E2,y)),X)) = X )
by FUNCT_3:def 3;
then
(
(chi ((E1 \/ E2),[:X,Y:])) . (
x,
y)
= 0 &
(chi ((Y-section (E1,y)),X)) . x = 0 &
(chi ((Y-section (E2,y)),X)) . x = 0 )
by C2, B1, FUNCT_1:def 2;
hence
(chi ((E1 \/ E2),[:X,Y:])) . (
x,
y)
= ((chi ((Y-section (E1,y)),X)) . x) + ((chi ((Y-section (E2,y)),X)) . x)
;
verum end; suppose C3:
(
x in X &
x in (Y-section (E1,y)) \/ (Y-section (E2,y)) )
;
(chi ((E1 \/ E2),[:X,Y:])) . (x,y) = ((chi ((Y-section (E1,y)),X)) . x) + ((chi ((Y-section (E2,y)),X)) . x)then C4:
(chi ((E1 \/ E2),[:X,Y:])) . (
x,
y)
= 1
by C2, FUNCT_3:def 3;
per cases
( ( x in Y-section (E1,y) & not x in Y-section (E2,y) ) or ( not x in Y-section (E1,y) & x in Y-section (E2,y) ) )
by A1, C3, XBOOLE_0:5;
suppose
(
x in Y-section (
E1,
y) & not
x in Y-section (
E2,
y) )
;
(chi ((E1 \/ E2),[:X,Y:])) . (x,y) = ((chi ((Y-section (E1,y)),X)) . x) + ((chi ((Y-section (E2,y)),X)) . x)then
(
(chi ((Y-section (E1,y)),X)) . x = 1 &
(chi ((Y-section (E2,y)),X)) . x = 0 )
by FUNCT_3:def 3;
hence
(chi ((E1 \/ E2),[:X,Y:])) . (
x,
y)
= ((chi ((Y-section (E1,y)),X)) . x) + ((chi ((Y-section (E2,y)),X)) . x)
by C4, XXREAL_3:4;
verum end; suppose
( not
x in Y-section (
E1,
y) &
x in Y-section (
E2,
y) )
;
(chi ((E1 \/ E2),[:X,Y:])) . (x,y) = ((chi ((Y-section (E1,y)),X)) . x) + ((chi ((Y-section (E2,y)),X)) . x)then
(
(chi ((Y-section (E1,y)),X)) . x = 0 &
(chi ((Y-section (E2,y)),X)) . x = 1 )
by FUNCT_3:def 3;
hence
(chi ((E1 \/ E2),[:X,Y:])) . (
x,
y)
= ((chi ((Y-section (E1,y)),X)) . x) + ((chi ((Y-section (E2,y)),X)) . x)
by C4, XXREAL_3:4;
verum end; end; end; suppose C5:
(
x in X & not
x in (Y-section (E1,y)) \/ (Y-section (E2,y)) )
;
(chi ((E1 \/ E2),[:X,Y:])) . (x,y) = ((chi ((Y-section (E1,y)),X)) . x) + ((chi ((Y-section (E2,y)),X)) . x)then C6:
(chi ((E1 \/ E2),[:X,Y:])) . (
x,
y)
= 0
by C2, FUNCT_3:def 3;
( not
x in Y-section (
E1,
y) & not
x in Y-section (
E2,
y) )
by C5, XBOOLE_0:def 3;
then
(
(chi ((Y-section (E1,y)),X)) . x = 0 &
(chi ((Y-section (E2,y)),X)) . x = 0 )
by C5, FUNCT_3:def 3;
hence
(chi ((E1 \/ E2),[:X,Y:])) . (
x,
y)
= ((chi ((Y-section (E1,y)),X)) . x) + ((chi ((Y-section (E2,y)),X)) . x)
by C6;
verum end; end;