let X, Y be non empty set ; 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 ; 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:]; ( (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
;
( (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;
verum end; suppose A4:
not
[x,y] in E
;
( (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
A7:
(chi ((X-section (E,x)),Y)) . y = 0
(chi ((Y-section (E,y)),X)) . x = 0
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;
verum end; end;