let C be composable with_identities preorder CategoryStr ; ( not C is empty implies ex F being Function of C,(RelOb C) st
( F is bijective & ( for f being morphism of C holds F . f = [(dom f),(cod f)] ) ) )
assume A1:
not C is empty
; ex F being Function of C,(RelOb C) st
( F is bijective & ( for f being morphism of C holds F . f = [(dom f),(cod f)] ) )
then reconsider C1 = C as non empty composable with_identities CategoryStr ;
defpred S1[ object , object ] means for f being morphism of C1 st $1 = f holds
$2 = [(dom f),(cod f)];
A2:
for x being Element of the carrier of C1 ex y being Element of RelOb C1 st S1[x,y]
consider F being Function of the carrier of C1,(RelOb C1) such that
A3:
for x being Element of the carrier of C1 holds S1[x,F . x]
from FUNCT_2:sch 3(A2);
reconsider F = F as Function of C,(RelOb C) ;
take
F
; ( F is bijective & ( for f being morphism of C holds F . f = [(dom f),(cod f)] ) )
for y being object st y in RelOb C holds
y in rng F
then
RelOb C1 c= rng F
by TARSKI:def 3;
then A7:
F is onto
by FUNCT_2:def 3, XBOOLE_0:def 10;
for x1, x2 being object st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds
x1 = x2
then
F is one-to-one
by FUNCT_1:def 4;
hence
F is bijective
by A7; for f being morphism of C holds F . f = [(dom f),(cod f)]
let f be morphism of C; F . f = [(dom f),(cod f)]
reconsider x = f as Element of the carrier of C1 by CAT_6:def 1;
thus F . f =
F . x
.=
[(dom f),(cod f)]
by A3
; verum