let A, B, C be set ; :: thesis: ( A c= B & A c= C implies (chi (B,B)) | A = (chi (C,C)) | A )
assume that
A1: A c= B and
A2: A c= C ; :: thesis: (chi (B,B)) | A = (chi (C,C)) | A
A3: now :: thesis: ( not A is empty implies (chi (B,B)) | A = (chi (C,C)) | A )
A4: dom ((chi (C,C)) | A) = (dom (chi (C,C))) /\ A by RELAT_1:61;
assume A5: not A is empty ; :: thesis: (chi (B,B)) | A = (chi (C,C)) | A
then not C is empty by ;
then dom ((chi (C,C)) | A) = C /\ A by ;
then A6: dom ((chi (C,C)) | A) = A by ;
A7: dom ((chi (B,B)) | A) = (dom (chi (B,B))) /\ A by RELAT_1:61;
not B is empty by ;
then dom ((chi (B,B)) | A) = B /\ A by ;
then A8: dom ((chi (B,B)) | A) = A by ;
now :: thesis: for x being object st x in A holds
((chi (B,B)) | A) . x = ((chi (C,C)) | A) . x
let x be object ; :: thesis: ( x in A implies ((chi (B,B)) | A) . x = ((chi (C,C)) | A) . x )
assume A9: x in A ; :: thesis: ((chi (B,B)) | A) . x = ((chi (C,C)) | A) . x
then ((chi (B,B)) | A) . x = (chi (B,B)) . x by ;
then ((chi (B,B)) | A) . x = 1 by ;
then ((chi (B,B)) | A) . x = (chi (C,C)) . x by ;
hence ((chi (B,B)) | A) . x = ((chi (C,C)) | A) . x by ; :: thesis: verum
end;
hence (chi (B,B)) | A = (chi (C,C)) | A by ; :: thesis: verum
end;
now :: thesis: ( A is empty implies (chi (B,B)) | A = (chi (C,C)) | A )
assume A10: A is empty ; :: thesis: (chi (B,B)) | A = (chi (C,C)) | A
then (chi (B,B)) | A = {} ;
hence (chi (B,B)) | A = (chi (C,C)) | A by A10; :: thesis: verum
end;
hence (chi (B,B)) | A = (chi (C,C)) | A by A3; :: thesis: verum