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

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;

end;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

hence
(chi (B,B)) | A = (chi (C,C)) | A
by A8, A6, FUNCT_1:2; :: thesis: verum((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;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

now :: thesis: ( A is empty implies (chi (B,B)) | A = (chi (C,C)) | A )

hence
(chi (B,B)) | A = (chi (C,C)) | A
by A3; :: thesis: verumassume 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;then (chi (B,B)) | A = {} ;

hence (chi (B,B)) | A = (chi (C,C)) | A by A10; :: thesis: verum