let X, Y be non empty set ; :: thesis: for x, y being set
for E being Subset of [:X,Y:] holds
( (chi (E,[:X,Y:])) . (x,y) = (chi ((X-section (E,x)),Y)) . y & (chi (E,[:X,Y:])) . (x,y) = (chi ((Y-section (E,y)),X)) . x )
let x, y be set ; :: thesis: for E being Subset of [:X,Y:] holds
( (chi (E,[:X,Y:])) . (x,y) = (chi ((X-section (E,x)),Y)) . y & (chi (E,[:X,Y:])) . (x,y) = (chi ((Y-section (E,y)),X)) . x )
let E be Subset of [:X,Y:]; :: thesis: ( (chi (E,[:X,Y:])) . (x,y) = (chi ((X-section (E,x)),Y)) . y & (chi (E,[:X,Y:])) . (x,y) = (chi ((Y-section (E,y)),X)) . x )
set z = [x,y];
per cases ( [x,y] in E or not [x,y] in E ) ;
suppose A1: [x,y] in E ; :: thesis: ( (chi (E,[:X,Y:])) . (x,y) = (chi ((X-section (E,x)),Y)) . y & (chi (E,[:X,Y:])) . (x,y) = (chi ((Y-section (E,y)),X)) . x )
then consider x1, y1 being object such that
A2: ( x1 in X & y1 in Y & [x,y] = [x1,y1] ) by ZFMISC_1:84;
( x = x1 & y = y1 ) by A2, XTUPLE_0:1;
then A3: ( y in X-section (E,x) & x in Y-section (E,y) ) by A1, A2;
(chi (E,[:X,Y:])) . [x,y] = 1 by A1, RFUNCT_1:63;
hence ( (chi (E,[:X,Y:])) . (x,y) = (chi ((X-section (E,x)),Y)) . y & (chi (E,[:X,Y:])) . (x,y) = (chi ((Y-section (E,y)),X)) . x ) by A3, RFUNCT_1:63; :: thesis: verum
end;
suppose A4: not [x,y] in E ; :: thesis: ( (chi (E,[:X,Y:])) . (x,y) = (chi ((X-section (E,x)),Y)) . y & (chi (E,[:X,Y:])) . (x,y) = (chi ((Y-section (E,y)),X)) . x )
A5: (chi (E,[:X,Y:])) . (x,y) = 0
proof
per cases ( [x,y] in [:X,Y:] or not [x,y] in [:X,Y:] ) ;
suppose [x,y] in [:X,Y:] ; :: thesis: (chi (E,[:X,Y:])) . (x,y) = 0
hence (chi (E,[:X,Y:])) . (x,y) = 0 by A4, FUNCT_3:def 3; :: thesis: verum
end;
suppose not [x,y] in [:X,Y:] ; :: thesis: (chi (E,[:X,Y:])) . (x,y) = 0
then not [x,y] in dom (chi (E,[:X,Y:])) ;
hence (chi (E,[:X,Y:])) . (x,y) = 0 by FUNCT_1:def 2; :: thesis: verum
end;
end;
end;
A6: now :: thesis: not y in X-section (E,x)
assume y in X-section (E,x) ; :: thesis: contradiction
then ex y1 being Element of Y st
( y = y1 & [x,y1] in E ) ;
hence contradiction by A4; :: thesis: verum
end;
A7: (chi ((X-section (E,x)),Y)) . y = 0
proof
per cases ( y in Y or not y in Y ) ;
suppose y in Y ; :: thesis: (chi ((X-section (E,x)),Y)) . y = 0
hence (chi ((X-section (E,x)),Y)) . y = 0 by A6, FUNCT_3:def 3; :: thesis: verum
end;
suppose not y in Y ; :: thesis: (chi ((X-section (E,x)),Y)) . y = 0
then not y in dom (chi ((X-section (E,x)),Y)) ;
hence (chi ((X-section (E,x)),Y)) . y = 0 by FUNCT_1:def 2; :: thesis: verum
end;
end;
end;
A8: now :: thesis: not x in Y-section (E,y)
assume x in Y-section (E,y) ; :: thesis: contradiction
then ex x1 being Element of X st
( x = x1 & [x1,y] in E ) ;
hence contradiction by A4; :: thesis: verum
end;
(chi ((Y-section (E,y)),X)) . x = 0
proof
per cases ( x in X or not x in X ) ;
suppose x in X ; :: thesis: (chi ((Y-section (E,y)),X)) . x = 0
hence (chi ((Y-section (E,y)),X)) . x = 0 by A8, FUNCT_3:def 3; :: thesis: verum
end;
suppose not x in X ; :: thesis: (chi ((Y-section (E,y)),X)) . x = 0
then not x in dom (chi ((Y-section (E,y)),X)) ;
hence (chi ((Y-section (E,y)),X)) . x = 0 by FUNCT_1:def 2; :: thesis: verum
end;
end;
end;
hence ( (chi (E,[:X,Y:])) . (x,y) = (chi ((X-section (E,x)),Y)) . y & (chi (E,[:X,Y:])) . (x,y) = (chi ((Y-section (E,y)),X)) . x ) by A5, A7; :: thesis: verum
end;
end;