let X be set ; :: thesis: for A1, A2 being Subset of X
for er being ExtReal
for x being object st A1 misses A2 holds
((chi (er,A1,X)) | A2) . x = 0
let A1, A2 be Subset of X; :: thesis: for er being ExtReal
for x being object st A1 misses A2 holds
((chi (er,A1,X)) | A2) . x = 0
let er be ExtReal; :: thesis: for x being object st A1 misses A2 holds
((chi (er,A1,X)) | A2) . x = 0
let x be object ; :: thesis: ( A1 misses A2 implies ((chi (er,A1,X)) | A2) . x = 0 )
assume a1: A1 misses A2 ; :: thesis: ((chi (er,A1,X)) | A2) . x = 0

per cases ( x in dom ((chi (er,A1,X)) | A2) or not x in dom ((chi (er,A1,X)) | A2) ) ;

suppose a2: x in dom ((chi (er,A1,X)) | A2) ; :: thesis: ((chi (er,A1,X)) | A2) . x = 0

then x in (dom (chi (er,A1,X))) /\ A2 by RELAT_1:61;
then ( x in X & x in A2 ) by XBOOLE_0:def 4;
then not x in A1 by a1, XBOOLE_0:3;
then (chi (er,A1,X)) . x = 0 by a2, Def1;
hence ((chi (er,A1,X)) | A2) . x = 0 by a2, FUNCT_1:47; :: thesis: verum

end;

suppose not x in dom ((chi (er,A1,X)) | A2) ; :: thesis: ((chi (er,A1,X)) | A2) . x = 0

hence ((chi (er,A1,X)) | A2) . x = 0 by FUNCT_1:def 2; :: thesis: verum

end;

end;