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 A2, XBOOLE_1:58, XBOOLE_1:61;
then dom ((chi (C,C)) | A) = C /\ A by A4, RFUNCT_1:61;
then A6: dom ((chi (C,C)) | A) = A by A2, XBOOLE_1:28;
A7: dom ((chi (B,B)) | A) = (dom (chi (B,B))) /\ A by RELAT_1:61;
not B is empty by A1, A5, XBOOLE_1:58, XBOOLE_1:61;
then dom ((chi (B,B)) | A) = B /\ A by A7, RFUNCT_1:61;
then A8: dom ((chi (B,B)) | A) = A by A1, XBOOLE_1:28;
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 A8, FUNCT_1:47;
then ((chi (B,B)) | A) . x = 1 by A1, A9, RFUNCT_1:61;
then ((chi (B,B)) | A) . x = (chi (C,C)) . x by A2, A9, RFUNCT_1:61;
hence ((chi (B,B)) | A) . x = ((chi (C,C)) | A) . x by A6, A9, FUNCT_1:47; :: thesis: verum
end;
hence (chi (B,B)) | A = (chi (C,C)) | A by A8, A6, FUNCT_1:2; :: 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