let X, Y be set ; :: thesis: for C being non empty set holds (chi (X,C)) (#) (chi (Y,C)) = chi ((X /\ Y),C)
let C be non empty set ; :: thesis: (chi (X,C)) (#) (chi (Y,C)) = chi ((X /\ Y),C)
A1: now :: thesis: 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)) . c
let c be Element of C; :: thesis: ( 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))) ; :: thesis: ((chi (X,C)) (#) (chi (Y,C))) . c = (chi ((X /\ Y),C)) . c
now :: thesis: ((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . c
per cases ( ((chi (X,C)) . c) * ((chi (Y,C)) . c) = 0 or ((chi (X,C)) . c) * ((chi (Y,C)) . c) <> 0 ) ;
suppose A2: ((chi (X,C)) . c) * ((chi (Y,C)) . c) = 0 ; :: thesis: ((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . c
now :: thesis: ((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . c
per cases ( (chi (X,C)) . c = 0 or (chi (Y,C)) . c = 0 ) by A2;
suppose (chi (X,C)) . c = 0 ; :: thesis: ((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . c
then not c in X by Th61;
then not c in X /\ Y by XBOOLE_0:def 4;
hence ((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . c by ; :: thesis: verum
end;
suppose (chi (Y,C)) . c = 0 ; :: thesis: ((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . c
then not c in Y by Th61;
then not c in X /\ Y by XBOOLE_0:def 4;
hence ((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . c by ; :: thesis: verum
end;
end;
end;
hence ((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . c ; :: thesis: verum
end;
suppose A3: ((chi (X,C)) . c) * ((chi (Y,C)) . c) <> 0 ; :: thesis: ((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . c
then A4: (chi (Y,C)) . c <> 0 ;
then A5: (chi (Y,C)) . c = 1 by Th67;
A6: c in Y by ;
A7: (chi (X,C)) . c <> 0 by A3;
then c in X by Th61;
then A8: c in X /\ Y by ;
(chi (X,C)) . c = 1 by ;
hence ((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . c by A5, A8, Th61; :: thesis: verum
end;
end;
end;
hence ((chi (X,C)) (#) (chi (Y,C))) . c = (chi ((X /\ Y),C)) . c by VALUED_1:5; :: thesis: 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 ; :: thesis: verum