let X, Y, A, B be set ; :: thesis: for x, y being object st x in X & y in Y holds
((chi (A,X)) . x) * ((chi (B,Y)) . y) = (chi ([:A,B:],[:X,Y:])) . (x,y)
let x, y be object ; :: thesis: ( x in X & y in Y implies ((chi (A,X)) . x) * ((chi (B,Y)) . y) = (chi ([:A,B:],[:X,Y:])) . (x,y) )
assume A1: ( x in X & y in Y ) ; :: thesis: ((chi (A,X)) . x) * ((chi (B,Y)) . y) = (chi ([:A,B:],[:X,Y:])) . (x,y)

per cases ( ( x in A & y in B ) or not x in A or not y in B ) ;

suppose A2: ( x in A & y in B ) ; :: thesis: ((chi (A,X)) . x) * ((chi (B,Y)) . y) = (chi ([:A,B:],[:X,Y:])) . (x,y)

then A3: ( [x,y] in [:X,Y:] & [x,y] in [:A,B:] ) by A1, ZFMISC_1:87;
( (chi (A,X)) . x = 1 & (chi (B,Y)) . y = 1 ) by A1, A2, FUNCT_3:def 3;
then ((chi (A,X)) . x) * ((chi (B,Y)) . y) = 1 * 1 by XXREAL_3:def 5;
hence ((chi (A,X)) . x) * ((chi (B,Y)) . y) = (chi ([:A,B:],[:X,Y:])) . (x,y) by A3, FUNCT_3:def 3; :: thesis: verum

end;

suppose A4: ( not x in A or not y in B ) ; :: thesis: ((chi (A,X)) . x) * ((chi (B,Y)) . y) = (chi ([:A,B:],[:X,Y:])) . (x,y)

then ( not [x,y] in [:A,B:] & [x,y] in [:X,Y:] ) by A1, ZFMISC_1:87;
then A5: (chi ([:A,B:],[:X,Y:])) . (x,y) = 0 by FUNCT_3:def 3;

per cases ( not x in A or not y in B ) by A4;

suppose not x in A ; :: thesis: ((chi (A,X)) . x) * ((chi (B,Y)) . y) = (chi ([:A,B:],[:X,Y:])) . (x,y)

then (chi (A,X)) . x = 0 by A1, FUNCT_3:def 3;
hence ((chi (A,X)) . x) * ((chi (B,Y)) . y) = (chi ([:A,B:],[:X,Y:])) . (x,y) by A5; :: thesis: verum

end;

suppose not y in B ; :: thesis: ((chi (A,X)) . x) * ((chi (B,Y)) . y) = (chi ([:A,B:],[:X,Y:])) . (x,y)

then (chi (B,Y)) . y = 0 by A1, FUNCT_3:def 3;
hence ((chi (A,X)) . x) * ((chi (B,Y)) . y) = (chi ([:A,B:],[:X,Y:])) . (x,y) by A5; :: thesis: verum

end;

end;

end;

end;