let C be composable with_identities preorder CategoryStr ; :: thesis: ( 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 ; :: thesis: 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 S₁[ 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 S₁[x,y]

proof

let x be Element of the carrier of C1; :: thesis: ex y being Element of RelOb C1 st S₁[x,y]
reconsider f = x as morphism of C1 by CAT_6:def 1;
set y = [(dom f),(cod f)];
f in Hom ((dom f),(cod f)) ;
then [(dom f),(cod f)] in RelOb C1 ;
then reconsider y = [(dom f),(cod f)] as Element of RelOb C1 ;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

consider F being Function of the carrier of C1,(RelOb C1) such that
A3: for x being Element of the carrier of C1 holds S₁[x,F . x] from FUNCT_2:sch 3(A2);
reconsider F = F as Function of C,(RelOb C) ;
take F ; :: thesis: ( 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

proof

let y be object ; :: thesis: ( y in RelOb C implies y in rng F )
assume y in RelOb C ; :: thesis: y in rng F
then consider a, b being Object of C such that
A4: ( y = [a,b] & ex f being morphism of C st f in Hom (a,b) ) ;
consider f being morphism of C such that
A5: f in Hom (a,b) by A4;
reconsider x = f as Element of C1 by CAT_6:def 1;
x in the carrier of C1 ;
then A6: x in dom F by FUNCT_2:def 1;
( a = dom f & b = cod f ) by A1, A5, Th20;
then F . x = [a,b] by A3;
hence y in rng F by A4, A6, FUNCT_1:3; :: thesis: verum

end;

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

proof

let x1, x2 be object ; :: thesis: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 implies x1 = x2 )
assume A8: ( x1 in dom F & x2 in dom F ) ; :: thesis: ( not F . x1 = F . x2 or x1 = x2 )
assume A9: F . x1 = F . x2 ; :: thesis: x1 = x2
reconsider x11 = x1, x22 = x2 as Element of the carrier of C1 by A8;
reconsider f1 = x11, f2 = x22 as morphism of C1 by CAT_6:def 1;
A10: F . f1 = [(dom f1),(cod f1)] by A3;
F . f2 = [(dom f2),(cod f2)] by A3;
then ( dom f1 = dom f2 & cod f1 = cod f2 ) by A10, A9, XTUPLE_0:1;
then ( f1 in Hom ((dom f1),(cod f1)) & f2 in Hom ((dom f1),(cod f1)) ) ;
hence x1 = x2 by Def12; :: thesis: verum

end;

then F is one-to-one by FUNCT_1:def 4;
hence F is bijective by A7; :: thesis: for f being morphism of C holds F . f = [(dom f),(cod f)]
let f be morphism of C; :: thesis: 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 ; :: thesis: verum