let X be set ; :: thesis: for A1, A2 being Subset of X
for er being ExtReal holds (chi (er,A1,X)) | A2 = (chi (er,(A1 /\ A2),X)) | A2
let A1, A2 be Subset of X; :: thesis: for er being ExtReal holds (chi (er,A1,X)) | A2 = (chi (er,(A1 /\ A2),X)) | A2
let er be ExtReal; :: thesis: (chi (er,A1,X)) | A2 = (chi (er,(A1 /\ A2),X)) | A2
a1: dom ((chi (er,A1,X)) | A2) = (dom (chi (er,A1,X))) /\ A2 by RELAT_1:61
.= X /\ A2 by FUNCT_2:def 1 ;
a2: dom ((chi (er,(A1 /\ A2),X)) | A2) = (dom (chi (er,(A1 /\ A2),X))) /\ A2 by RELAT_1:61
.= dom ((chi (er,A1,X)) | A2) by a1, FUNCT_2:def 1 ;

now :: thesis: for x being Element of X st x in dom ((chi (er,A1,X)) | A2) holds
((chi (er,(A1 /\ A2),X)) | A2) . x = ((chi (er,A1,X)) | A2) . x

let x be Element of X; :: thesis: ( x in dom ((chi (er,A1,X)) | A2) implies ((chi (er,(A1 /\ A2),X)) | A2) . b₁ = ((chi (er,A1,X)) | A2) . b₁ )
assume b1: x in dom ((chi (er,A1,X)) | A2) ; :: thesis: ((chi (er,(A1 /\ A2),X)) | A2) . b₁ = ((chi (er,A1,X)) | A2) . b₁
then a3: ( x in X & x in A2 ) by a1, XBOOLE_0:def 4;
then a4: ( ((chi (er,A1,X)) | A2) . x = (chi (er,A1,X)) . x & ((chi (er,(A1 /\ A2),X)) | A2) . x = (chi (er,(A1 /\ A2),X)) . x ) by FUNCT_1:49;

per cases ( x in A1 or not x in A1 ) ;

suppose a5: x in A1 ; :: thesis: ((chi (er,(A1 /\ A2),X)) | A2) . b₁ = ((chi (er,A1,X)) | A2) . b₁

then a6: ((chi (er,A1,X)) | A2) . x = er by a4, Def1;
x in A1 /\ A2 by a3, a5, XBOOLE_0:def 4;
hence ((chi (er,(A1 /\ A2),X)) | A2) . x = ((chi (er,A1,X)) | A2) . x by a4, a6, Def1; :: thesis: verum

end;

suppose a7: not x in A1 ; :: thesis: ((chi (er,(A1 /\ A2),X)) | A2) . b₁ = ((chi (er,A1,X)) | A2) . b₁

then a8: ((chi (er,A1,X)) | A2) . x = 0 by a4, Def1, b1;
not x in A1 /\ A2 by a7, XBOOLE_0:def 4;
hence ((chi (er,(A1 /\ A2),X)) | A2) . x = ((chi (er,A1,X)) | A2) . x by b1, a4, a8, Def1; :: thesis: verum

end;

end;

end;

hence (chi (er,A1,X)) | A2 = (chi (er,(A1 /\ A2),X)) | A2 by a2, PARTFUN1:5; :: thesis: verum