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

A4: dom ((chi C,C) | A) = (dom (chi C,C)) /\ A by RELAT_1:90;
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:77;
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:90;
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:77;
then A8: dom ((chi B,B) | A) = A by A1, XBOOLE_1:28;

now

let x be set ; :: 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:70;
then ((chi B,B) | A) . x = 1 by A1, A9, RFUNCT_1:77;
then ((chi B,B) | A) . x = (chi C,C) . x by A2, A9, RFUNCT_1:77;
hence ((chi B,B) | A) . x = ((chi C,C) | A) . x by A6, A9, FUNCT_1:70; :: thesis: verum

end;

hence (chi B,B) | A = (chi C,C) | A by A8, A6, FUNCT_1:9; :: thesis: verum

end;

now

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