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

end;

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;hence ( dom (RelOb C) = Ob C & rng (RelOb C) = Ob C ) ; :: thesis: verum

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)

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)

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

end;x in dom (RelOb C)

proof

then
Ob C c= dom (RelOb C)
by TARSKI:def 3;
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;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

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

then
Ob C c= rng (RelOb C)
by TARSKI:def 3;
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;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

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