let C be composable with_identities CategoryStr ; :: thesis: ( dom (RelOb C) = Ob C & rng (RelOb C) = Ob C )

per cases ( C is empty or not C is empty ) ;

suppose C is empty ; :: thesis: ( dom (RelOb C) = Ob C & rng (RelOb C) = Ob C )

then ( Ob C = {} & RelOb C = {} ) ;
hence ( dom (RelOb C) = Ob C & rng (RelOb C) = Ob C ) ; :: thesis: verum

end;

suppose A1: not C is empty ; :: thesis: ( dom (RelOb C) = Ob C & rng (RelOb C) = Ob C )

for x being object st x in Ob C holds
x in dom (RelOb C)

proof

let x be object ; :: thesis: ( x in Ob C implies x in dom (RelOb C) )
assume A2: x in Ob C ; :: thesis: x in dom (RelOb C)
then reconsider o = x as Object of C ;
reconsider f = o as morphism of C by A2;
f is identity by A1, CAT_6:22;
then A3: ( dom f = o & cod f = o ) by Th6;
f in Hom ((dom f),(cod f)) by A1, Th19;
then [o,o] in RelOb C by A3;
hence x in dom (RelOb C) by XTUPLE_0:def 12; :: thesis: verum

end;

then Ob C c= dom (RelOb C) by TARSKI:def 3;
hence dom (RelOb C) = Ob C by XBOOLE_0:def 10; :: thesis: rng (RelOb C) = Ob C
for x being object st x in Ob C holds
x in rng (RelOb C)

proof

let x be object ; :: thesis: ( x in Ob C implies x in rng (RelOb C) )
assume A4: x in Ob C ; :: thesis: x in rng (RelOb C)
then reconsider o = x as Object of C ;
reconsider f = o as morphism of C by A4;
f is identity by A1, CAT_6:22;
then A5: ( dom f = o & cod f = o ) by Th6;
f in Hom ((dom f),(cod f)) by A1, Th19;
then [o,o] in RelOb C by A5;
hence x in rng (RelOb C) by XTUPLE_0:def 13; :: thesis: verum

end;

then Ob C c= rng (RelOb C) by TARSKI:def 3;
hence rng (RelOb C) = Ob C by XBOOLE_0:def 10; :: thesis: verum

end;

end;