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

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

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

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 Th77;
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 A2, Th77; :: 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 Th77;
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 A2, Th77; :: 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 Th84;
A6: c in Y by A4, Th77;
A7: (chi X,C) . c <> 0 by A3;
then c in X by Th77;
then A8: c in X /\ Y by A6, XBOOLE_0:def 4;
(chi X,C) . c = 1 by A7, Th84;
hence ((chi X,C) . c) * ((chi Y,C) . c) = (chi (X /\ Y),C) . c by A5, A8, Th77; :: 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 Th77
.= C /\ C by Th77
.= dom (chi (X /\ Y),C) by Th77 ;
hence (chi X,C) (#) (chi Y,C) = chi (X /\ Y),C by A1, PARTFUN1:34; :: thesis: verum