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_{1}[ 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_{1}[x,y]

A3: for x being Element of the carrier of C1 holds S_{1}[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

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

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

( 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

$2 = [(dom f),(cod f)];

A2: for x being Element of the carrier of C1 ex y being Element of RelOb C1 st S

proof

consider F being Function of the carrier of C1,(RelOb C1) such that
let x be Element of the carrier of C1; :: thesis: ex y being Element of RelOb C1 st S_{1}[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_{1}[x,y]

thus S_{1}[x,y]
; :: thesis: verum

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

thus S

A3: for x being Element of the carrier of C1 holds S

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

then
RelOb C1 c= rng F
by TARSKI:def 3;
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;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

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

then
F is one-to-one
by FUNCT_1:def 4;
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;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

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