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;