let X, Y be set ; for C being non empty set holds (chi (X,C)) (#) (chi (Y,C)) = chi ((X /\ Y),C)
let C be non empty set ; (chi (X,C)) (#) (chi (Y,C)) = chi ((X /\ Y),C)
A1:
now for c being Element of C st c in dom ((chi (X,C)) (#) (chi (Y,C))) holds
((chi (X,C)) (#) (chi (Y,C))) . c = (chi ((X /\ Y),C)) . clet c be
Element of
C;
( c in dom ((chi (X,C)) (#) (chi (Y,C))) implies ((chi (X,C)) (#) (chi (Y,C))) . c = (chi ((X /\ Y),C)) . c )assume
c in dom ((chi (X,C)) (#) (chi (Y,C)))
;
((chi (X,C)) (#) (chi (Y,C))) . c = (chi ((X /\ Y),C)) . cnow ((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . cper cases
( ((chi (X,C)) . c) * ((chi (Y,C)) . c) = 0 or ((chi (X,C)) . c) * ((chi (Y,C)) . c) <> 0 )
;
suppose A3:
((chi (X,C)) . c) * ((chi (Y,C)) . c) <> 0
;
((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . cthen A4:
(chi (Y,C)) . c <> 0
;
then A5:
(chi (Y,C)) . c = 1
by Th67;
A6:
c in Y
by A4, Th61;
A7:
(chi (X,C)) . c <> 0
by A3;
then
c in X
by Th61;
then A8:
c in X /\ Y
by A6, XBOOLE_0:def 4;
(chi (X,C)) . c = 1
by A7, Th67;
hence
((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . c
by A5, A8, Th61;
verum end; end; end; hence
((chi (X,C)) (#) (chi (Y,C))) . c = (chi ((X /\ Y),C)) . c
by VALUED_1:5;
verum end;
dom ((chi (X,C)) (#) (chi (Y,C))) =
(dom (chi (X,C))) /\ (dom (chi (Y,C)))
by VALUED_1:def 4
.=
C /\ (dom (chi (Y,C)))
by Th61
.=
C /\ C
by Th61
.=
dom (chi ((X /\ Y),C))
by Th61
;
hence
(chi (X,C)) (#) (chi (Y,C)) = chi ((X /\ Y),C)
by A1, PARTFUN1:5; verum