let X, Y be non empty set ; :: thesis: 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 ; :: thesis: 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:]; :: thesis: ( 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 ; :: thesis: ( (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) :: thesis: (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 ; :: thesis: (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) ; :: thesis: verum

end;

suppose A3: ( y in Y & y in (X-section (E1,x)) \/ (X-section (E2,x)) ) ; :: thesis: (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) ) ; :: thesis: (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; :: thesis: verum

end;

suppose ( not y in X-section (E1,x) & y in X-section (E2,x) ) ; :: thesis: (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; :: thesis: verum

end;

end;

end;

suppose A5: ( y in Y & not y in (X-section (E1,x)) \/ (X-section (E2,x)) ) ; :: thesis: (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; :: thesis: 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 ; :: thesis: (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) ; :: thesis: verum

end;

suppose C3: ( x in X & x in (Y-section (E1,y)) \/ (Y-section (E2,y)) ) ; :: thesis: (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) ) ; :: thesis: (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; :: thesis: verum

end;

suppose ( not x in Y-section (E1,y) & x in Y-section (E2,y) ) ; :: thesis: (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; :: thesis: verum

end;

end;

end;

suppose C5: ( x in X & not x in (Y-section (E1,y)) \/ (Y-section (E2,y)) ) ; :: thesis: (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; :: thesis: verum

end;

end;