let O1, O2 be ordinal number ; :: thesis: for C1 being preorder O1 -ordered category

for C2 being preorder O2 -ordered category holds

( O1 = O2 iff C1 ~= C2 )

let C1 be preorder O1 -ordered category; :: thesis: for C2 being preorder O2 -ordered category holds

( O1 = O2 iff C1 ~= C2 )

let C2 be preorder O2 -ordered category; :: thesis: ( O1 = O2 iff C1 ~= C2 )

thus ( O1 = O2 implies C1 ~= C2 ) :: thesis: ( C1 ~= C2 implies O1 = O2 )

for C2 being preorder O2 -ordered category holds

( O1 = O2 iff C1 ~= C2 )

let C1 be preorder O1 -ordered category; :: thesis: for C2 being preorder O2 -ordered category holds

( O1 = O2 iff C1 ~= C2 )

let C2 be preorder O2 -ordered category; :: thesis: ( O1 = O2 iff C1 ~= C2 )

thus ( O1 = O2 implies C1 ~= C2 ) :: thesis: ( C1 ~= C2 implies O1 = O2 )

proof

thus
( C1 ~= C2 implies O1 = O2 )
:: thesis: verum
assume A1:
O1 = O2
; :: thesis: C1 ~= C2

end;per cases
( O1 is empty or not O1 is empty )
;

end;

suppose A2:
not O1 is empty
; :: thesis: C1 ~= C2

then reconsider D1 = C1, D2 = C2 as non empty category by A1;

consider F1 being Function such that

A3: F1 is_isomorphism_of RelOb C1, RelIncl O1 by Def14, WELLORD1:def 8;

consider F2 being Function such that

A4: F2 is_isomorphism_of RelOb C2, RelIncl O2 by Def14, WELLORD1:def 8;

A5: F2 " is_isomorphism_of RelIncl O2, RelOb C2 by A4, WELLORD1:39;

set F3 = (F2 ") * F1;

A6: (F2 ") * F1 is_isomorphism_of RelOb C1, RelOb C2 by A1, A3, A5, WELLORD1:41;

consider F4 being Function of C1,(RelOb C1) such that

A7: ( F4 is bijective & ( for f being morphism of C1 holds F4 . f = [(dom f),(cod f)] ) ) by A2, Th36;

consider F5 being Function of C2,(RelOb C2) such that

A8: ( F5 is bijective & ( for f being morphism of C2 holds F5 . f = [(dom f),(cod f)] ) ) by A1, A2, Th36;

A9: ( dom ((F2 ") * F1) = field (RelOb C1) & rng ((F2 ") * F1) = field (RelOb C2) & (F2 ") * F1 is one-to-one & ( for a, b being set holds

( [a,b] in RelOb C1 iff ( a in field (RelOb C1) & b in field (RelOb C1) & [(((F2 ") * F1) . a),(((F2 ") * F1) . b)] in RelOb C2 ) ) ) ) by A6, WELLORD1:def 7;

A10: field (RelOb C1) = (dom (RelOb C1)) \/ (rng (RelOb C1)) by RELAT_1:def 6

.= (dom (RelOb C1)) \/ (Ob C1) by Th34

.= (Ob C1) \/ (Ob C1) by Th34

.= Ob C1 ;

defpred S_{1}[ object , object ] means for a, b being set st $1 = [a,b] holds

$2 = [(((F2 ") * F1) . a),(((F2 ") * F1) . b)];

A11: for x being Element of RelOb D1 ex y being Element of RelOb D2 st S_{1}[x,y]

A13: for x being Element of RelOb D1 holds S_{1}[x,F33 . x]
from FUNCT_2:sch 3(A11);

A14: ( rng F5 = dom (F5 ") & dom F5 = rng (F5 ") ) by A8, FUNCT_1:33;

set F = ((F5 ") * F33) * F4;

rng F33 c= RelOb C2 ;

then rng F33 c= rng F5 by A8, FUNCT_2:def 3;

then A15: dom ((F5 ") * F33) = dom F33 by A14, RELAT_1:27;

RelOb C1 c= dom F33 by FUNCT_2:def 1;

then rng F4 c= dom F33 by XBOOLE_1:1;

then A16: dom (((F5 ") * F33) * F4) = dom F4 by A15, RELAT_1:27;

then A17: dom (((F5 ") * F33) * F4) = the carrier of C1 by FUNCT_2:def 1;

for y being object st y in RelOb C2 holds

y in rng F33

then rng F5 c= rng F33 by A8, FUNCT_2:def 3;

then rng ((F5 ") * F33) = rng (F5 ") by A14, RELAT_1:28;

then A24: rng ((F5 ") * F33) = the carrier of C2 by A14, FUNCT_2:def 1;

dom F33 c= RelOb C1 ;

then dom F33 c= rng F4 by A7, FUNCT_2:def 3;

then A25: rng (((F5 ") * F33) * F4) = the carrier of C2 by A24, A15, RELAT_1:28;

then reconsider F = ((F5 ") * F33) * F4 as Functor of C1,C2 by A17, FUNCT_2:1;

for x1, x2 being object st x1 in dom F33 & x2 in dom F33 & F33 . x1 = F33 . x2 holds

x1 = x2

A32: F is onto by A25, FUNCT_2:def 3;

A33: for f being morphism of C1 holds

( dom (F . f) = ((F2 ") * F1) . (dom f) & cod (F . f) = ((F2 ") * F1) . (cod f) )

( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) )

for f being morphism of C1 st f is identity holds

F . f is identity

hence C1 ~= C2 by A32, Th12, A45, CAT_6:def 25, A8, A7, A31; :: thesis: verum

end;consider F1 being Function such that

A3: F1 is_isomorphism_of RelOb C1, RelIncl O1 by Def14, WELLORD1:def 8;

consider F2 being Function such that

A4: F2 is_isomorphism_of RelOb C2, RelIncl O2 by Def14, WELLORD1:def 8;

A5: F2 " is_isomorphism_of RelIncl O2, RelOb C2 by A4, WELLORD1:39;

set F3 = (F2 ") * F1;

A6: (F2 ") * F1 is_isomorphism_of RelOb C1, RelOb C2 by A1, A3, A5, WELLORD1:41;

consider F4 being Function of C1,(RelOb C1) such that

A7: ( F4 is bijective & ( for f being morphism of C1 holds F4 . f = [(dom f),(cod f)] ) ) by A2, Th36;

consider F5 being Function of C2,(RelOb C2) such that

A8: ( F5 is bijective & ( for f being morphism of C2 holds F5 . f = [(dom f),(cod f)] ) ) by A1, A2, Th36;

A9: ( dom ((F2 ") * F1) = field (RelOb C1) & rng ((F2 ") * F1) = field (RelOb C2) & (F2 ") * F1 is one-to-one & ( for a, b being set holds

( [a,b] in RelOb C1 iff ( a in field (RelOb C1) & b in field (RelOb C1) & [(((F2 ") * F1) . a),(((F2 ") * F1) . b)] in RelOb C2 ) ) ) ) by A6, WELLORD1:def 7;

A10: field (RelOb C1) = (dom (RelOb C1)) \/ (rng (RelOb C1)) by RELAT_1:def 6

.= (dom (RelOb C1)) \/ (Ob C1) by Th34

.= (Ob C1) \/ (Ob C1) by Th34

.= Ob C1 ;

defpred S

$2 = [(((F2 ") * F1) . a),(((F2 ") * F1) . b)];

A11: for x being Element of RelOb D1 ex y being Element of RelOb D2 st S

proof

consider F33 being Function of (RelOb D1),(RelOb D2) such that
let x be Element of RelOb D1; :: thesis: ex y being Element of RelOb D2 st S_{1}[x,y]

x in RelOb D1 ;

then consider o1, o2 being Object of D1 such that

A12: ( x = [o1,o2] & ex f being morphism of D1 st f in Hom (o1,o2) ) ;

reconsider y = [(((F2 ") * F1) . o1),(((F2 ") * F1) . o2)] as Element of RelOb D2 by A12, A6, WELLORD1:def 7;

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

for a, b being set st x = [a,b] holds

y = [(((F2 ") * F1) . a),(((F2 ") * F1) . b)]_{1}[x,y]
; :: thesis: verum

end;x in RelOb D1 ;

then consider o1, o2 being Object of D1 such that

A12: ( x = [o1,o2] & ex f being morphism of D1 st f in Hom (o1,o2) ) ;

reconsider y = [(((F2 ") * F1) . o1),(((F2 ") * F1) . o2)] as Element of RelOb D2 by A12, A6, WELLORD1:def 7;

take y ; :: thesis: S

for a, b being set st x = [a,b] holds

y = [(((F2 ") * F1) . a),(((F2 ") * F1) . b)]

proof

hence
S
let a, b be set ; :: thesis: ( x = [a,b] implies y = [(((F2 ") * F1) . a),(((F2 ") * F1) . b)] )

assume x = [a,b] ; :: thesis: y = [(((F2 ") * F1) . a),(((F2 ") * F1) . b)]

then ( a = o1 & b = o2 ) by A12, XTUPLE_0:1;

hence y = [(((F2 ") * F1) . a),(((F2 ") * F1) . b)] ; :: thesis: verum

end;assume x = [a,b] ; :: thesis: y = [(((F2 ") * F1) . a),(((F2 ") * F1) . b)]

then ( a = o1 & b = o2 ) by A12, XTUPLE_0:1;

hence y = [(((F2 ") * F1) . a),(((F2 ") * F1) . b)] ; :: thesis: verum

A13: for x being Element of RelOb D1 holds S

A14: ( rng F5 = dom (F5 ") & dom F5 = rng (F5 ") ) by A8, FUNCT_1:33;

set F = ((F5 ") * F33) * F4;

rng F33 c= RelOb C2 ;

then rng F33 c= rng F5 by A8, FUNCT_2:def 3;

then A15: dom ((F5 ") * F33) = dom F33 by A14, RELAT_1:27;

RelOb C1 c= dom F33 by FUNCT_2:def 1;

then rng F4 c= dom F33 by XBOOLE_1:1;

then A16: dom (((F5 ") * F33) * F4) = dom F4 by A15, RELAT_1:27;

then A17: dom (((F5 ") * F33) * F4) = the carrier of C1 by FUNCT_2:def 1;

for y being object st y in RelOb C2 holds

y in rng F33

proof

then
RelOb C2 c= rng F33
by TARSKI:def 3;
let y be object ; :: thesis: ( y in RelOb C2 implies y in rng F33 )

assume y in RelOb C2 ; :: thesis: y in rng F33

then consider o1, o2 being Object of C2 such that

A18: ( y = [o1,o2] & ex g being morphism of C2 st g in Hom (o1,o2) ) ;

A19: rng ((F2 ") * F1) = (dom (RelOb C2)) \/ (rng (RelOb C2)) by A9, RELAT_1:def 6

.= (dom (RelOb C2)) \/ (Ob C2) by Th34

.= (Ob C2) \/ (Ob C2) by Th34

.= Ob D2 ;

consider x1 being object such that

A20: ( x1 in dom ((F2 ") * F1) & o1 = ((F2 ") * F1) . x1 ) by A19, FUNCT_1:def 3;

consider x2 being object such that

A21: ( x2 in dom ((F2 ") * F1) & o2 = ((F2 ") * F1) . x2 ) by A19, FUNCT_1:def 3;

reconsider x1 = x1, x2 = x2 as set by A20, A21;

set x = [x1,x2];

A22: ( x1 in field (RelOb C1) & x2 in field (RelOb C1) ) by A20, A21, A6, WELLORD1:def 7;

[(((F2 ") * F1) . x1),(((F2 ") * F1) . x2)] in RelOb C2 by A18, A20, A21;

then reconsider x = [x1,x2] as Element of RelOb D1 by A22, A6, WELLORD1:def 7;

A23: dom F33 = RelOb D1 by FUNCT_2:def 1;

F33 . x = [(((F2 ") * F1) . x1),(((F2 ") * F1) . x2)] by A13;

hence y in rng F33 by A23, A18, A20, A21, FUNCT_1:def 3; :: thesis: verum

end;assume y in RelOb C2 ; :: thesis: y in rng F33

then consider o1, o2 being Object of C2 such that

A18: ( y = [o1,o2] & ex g being morphism of C2 st g in Hom (o1,o2) ) ;

A19: rng ((F2 ") * F1) = (dom (RelOb C2)) \/ (rng (RelOb C2)) by A9, RELAT_1:def 6

.= (dom (RelOb C2)) \/ (Ob C2) by Th34

.= (Ob C2) \/ (Ob C2) by Th34

.= Ob D2 ;

consider x1 being object such that

A20: ( x1 in dom ((F2 ") * F1) & o1 = ((F2 ") * F1) . x1 ) by A19, FUNCT_1:def 3;

consider x2 being object such that

A21: ( x2 in dom ((F2 ") * F1) & o2 = ((F2 ") * F1) . x2 ) by A19, FUNCT_1:def 3;

reconsider x1 = x1, x2 = x2 as set by A20, A21;

set x = [x1,x2];

A22: ( x1 in field (RelOb C1) & x2 in field (RelOb C1) ) by A20, A21, A6, WELLORD1:def 7;

[(((F2 ") * F1) . x1),(((F2 ") * F1) . x2)] in RelOb C2 by A18, A20, A21;

then reconsider x = [x1,x2] as Element of RelOb D1 by A22, A6, WELLORD1:def 7;

A23: dom F33 = RelOb D1 by FUNCT_2:def 1;

F33 . x = [(((F2 ") * F1) . x1),(((F2 ") * F1) . x2)] by A13;

hence y in rng F33 by A23, A18, A20, A21, FUNCT_1:def 3; :: thesis: verum

then rng F5 c= rng F33 by A8, FUNCT_2:def 3;

then rng ((F5 ") * F33) = rng (F5 ") by A14, RELAT_1:28;

then A24: rng ((F5 ") * F33) = the carrier of C2 by A14, FUNCT_2:def 1;

dom F33 c= RelOb C1 ;

then dom F33 c= rng F4 by A7, FUNCT_2:def 3;

then A25: rng (((F5 ") * F33) * F4) = the carrier of C2 by A24, A15, RELAT_1:28;

then reconsider F = ((F5 ") * F33) * F4 as Functor of C1,C2 by A17, FUNCT_2:1;

for x1, x2 being object st x1 in dom F33 & x2 in dom F33 & F33 . x1 = F33 . x2 holds

x1 = x2

proof

then A31:
F33 is one-to-one
by FUNCT_1:def 4;
let x1, x2 be object ; :: thesis: ( x1 in dom F33 & x2 in dom F33 & F33 . x1 = F33 . x2 implies x1 = x2 )

assume x1 in dom F33 ; :: thesis: ( not x2 in dom F33 or not F33 . x1 = F33 . x2 or x1 = x2 )

then x1 in RelOb D1 ;

then consider o11, o12 being Object of D1 such that

A26: ( x1 = [o11,o12] & ex f1 being morphism of D1 st f1 in Hom (o11,o12) ) ;

A27: [o11,o12] in RelOb C1 by A26;

reconsider x11 = x1 as Element of RelOb D1 by A26, A27;

assume x2 in dom F33 ; :: thesis: ( not F33 . x1 = F33 . x2 or x1 = x2 )

then x2 in RelOb D1 ;

then consider o21, o22 being Object of D1 such that

A28: ( x2 = [o21,o22] & ex f1 being morphism of D1 st f1 in Hom (o21,o22) ) ;

A29: [o21,o22] in RelOb C1 by A28;

reconsider x22 = x2 as Element of RelOb D1 by A28, A29;

assume A30: F33 . x1 = F33 . x2 ; :: thesis: x1 = x2

( F33 . x11 = [(((F2 ") * F1) . o11),(((F2 ") * F1) . o12)] & F33 . x22 = [(((F2 ") * F1) . o21),(((F2 ") * F1) . o22)] ) by A13, A26, A28;

then ( ((F2 ") * F1) . o11 = ((F2 ") * F1) . o21 & ((F2 ") * F1) . o12 = ((F2 ") * F1) . o22 ) by A30, XTUPLE_0:1;

then ( o11 = o21 & o12 = o22 ) by A10, A9, FUNCT_1:def 4;

hence x1 = x2 by A26, A28; :: thesis: verum

end;assume x1 in dom F33 ; :: thesis: ( not x2 in dom F33 or not F33 . x1 = F33 . x2 or x1 = x2 )

then x1 in RelOb D1 ;

then consider o11, o12 being Object of D1 such that

A26: ( x1 = [o11,o12] & ex f1 being morphism of D1 st f1 in Hom (o11,o12) ) ;

A27: [o11,o12] in RelOb C1 by A26;

reconsider x11 = x1 as Element of RelOb D1 by A26, A27;

assume x2 in dom F33 ; :: thesis: ( not F33 . x1 = F33 . x2 or x1 = x2 )

then x2 in RelOb D1 ;

then consider o21, o22 being Object of D1 such that

A28: ( x2 = [o21,o22] & ex f1 being morphism of D1 st f1 in Hom (o21,o22) ) ;

A29: [o21,o22] in RelOb C1 by A28;

reconsider x22 = x2 as Element of RelOb D1 by A28, A29;

assume A30: F33 . x1 = F33 . x2 ; :: thesis: x1 = x2

( F33 . x11 = [(((F2 ") * F1) . o11),(((F2 ") * F1) . o12)] & F33 . x22 = [(((F2 ") * F1) . o21),(((F2 ") * F1) . o22)] ) by A13, A26, A28;

then ( ((F2 ") * F1) . o11 = ((F2 ") * F1) . o21 & ((F2 ") * F1) . o12 = ((F2 ") * F1) . o22 ) by A30, XTUPLE_0:1;

then ( o11 = o21 & o12 = o22 ) by A10, A9, FUNCT_1:def 4;

hence x1 = x2 by A26, A28; :: thesis: verum

A32: F is onto by A25, FUNCT_2:def 3;

A33: for f being morphism of C1 holds

( dom (F . f) = ((F2 ") * F1) . (dom f) & cod (F . f) = ((F2 ") * F1) . (cod f) )

proof

for f1, f2 being morphism of C1 st f1 |> f2 holds
let f be morphism of C1; :: thesis: ( dom (F . f) = ((F2 ") * F1) . (dom f) & cod (F . f) = ((F2 ") * F1) . (cod f) )

reconsider x = f as object ;

x in Mor C1 by A2, SUBSET_1:def 1;

then A34: x in dom F4 by A17, A16, CAT_6:def 1;

f in Hom ((dom f),(cod f)) by A2, Th20;

then A35: [(dom f),(cod f)] in RelOb D1 ;

then A36: [(dom f),(cod f)] in dom F33 by FUNCT_2:def 1;

reconsider x1 = [(dom f),(cod f)] as Element of RelOb D1 by A35;

A37: for a, b being set st x1 = [a,b] holds

F33 . x1 = [(((F2 ") * F1) . a),(((F2 ") * F1) . b)] by A13;

[(((F2 ") * F1) . (dom f)),(((F2 ") * F1) . (cod f))] in RelOb C2 by A35, A6, WELLORD1:def 7;

then A38: [(((F2 ") * F1) . (dom f)),(((F2 ") * F1) . (cod f))] in rng F5 by A8, FUNCT_2:def 3;

A39: F . f = (((F5 ") * F33) * F4) . x by CAT_6:def 21

.= ((F5 ") * F33) . (F4 . x) by A34, FUNCT_1:13

.= ((F5 ") * F33) . [(dom f),(cod f)] by A7

.= (F5 ") . (F33 . [(dom f),(cod f)]) by A36, FUNCT_1:13

.= (F5 ") . [(((F2 ") * F1) . (dom f)),(((F2 ") * F1) . (cod f))] by A37 ;

[(dom (F . f)),(cod (F . f))] = F5 . ((F5 ") . [(((F2 ") * F1) . (dom f)),(((F2 ") * F1) . (cod f))]) by A8, A39

.= [(((F2 ") * F1) . (dom f)),(((F2 ") * F1) . (cod f))] by A8, A38, FUNCT_1:35 ;

hence ( dom (F . f) = ((F2 ") * F1) . (dom f) & cod (F . f) = ((F2 ") * F1) . (cod f) ) by XTUPLE_0:1; :: thesis: verum

end;reconsider x = f as object ;

x in Mor C1 by A2, SUBSET_1:def 1;

then A34: x in dom F4 by A17, A16, CAT_6:def 1;

f in Hom ((dom f),(cod f)) by A2, Th20;

then A35: [(dom f),(cod f)] in RelOb D1 ;

then A36: [(dom f),(cod f)] in dom F33 by FUNCT_2:def 1;

reconsider x1 = [(dom f),(cod f)] as Element of RelOb D1 by A35;

A37: for a, b being set st x1 = [a,b] holds

F33 . x1 = [(((F2 ") * F1) . a),(((F2 ") * F1) . b)] by A13;

[(((F2 ") * F1) . (dom f)),(((F2 ") * F1) . (cod f))] in RelOb C2 by A35, A6, WELLORD1:def 7;

then A38: [(((F2 ") * F1) . (dom f)),(((F2 ") * F1) . (cod f))] in rng F5 by A8, FUNCT_2:def 3;

A39: F . f = (((F5 ") * F33) * F4) . x by CAT_6:def 21

.= ((F5 ") * F33) . (F4 . x) by A34, FUNCT_1:13

.= ((F5 ") * F33) . [(dom f),(cod f)] by A7

.= (F5 ") . (F33 . [(dom f),(cod f)]) by A36, FUNCT_1:13

.= (F5 ") . [(((F2 ") * F1) . (dom f)),(((F2 ") * F1) . (cod f))] by A37 ;

[(dom (F . f)),(cod (F . f))] = F5 . ((F5 ") . [(((F2 ") * F1) . (dom f)),(((F2 ") * F1) . (cod f))]) by A8, A39

.= [(((F2 ") * F1) . (dom f)),(((F2 ") * F1) . (cod f))] by A8, A38, FUNCT_1:35 ;

hence ( dom (F . f) = ((F2 ") * F1) . (dom f) & cod (F . f) = ((F2 ") * F1) . (cod f) ) by XTUPLE_0:1; :: thesis: verum

( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) )

proof

then A45:
F is multiplicative
by CAT_6:def 23;
let f1, f2 be morphism of C1; :: thesis: ( f1 |> f2 implies ( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) ) )

assume A40: f1 |> f2 ; :: thesis: ( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) )

dom (F . f1) = ((F2 ") * F1) . (dom f1) by A33

.= ((F2 ") * F1) . (cod f2) by A2, A40, Th5

.= cod (F . f2) by A33 ;

hence A41: F . f1 |> F . f2 by Th5; :: thesis: F . (f1 (*) f2) = (F . f1) (*) (F . f2)

set g1 = F . (f1 (*) f2);

set g2 = (F . f1) (*) (F . f2);

A42: dom (F . (f1 (*) f2)) = ((F2 ") * F1) . (dom (f1 (*) f2)) by A33

.= ((F2 ") * F1) . (dom f2) by A40, Th4

.= dom (F . f2) by A33

.= dom ((F . f1) (*) (F . f2)) by A41, Th4 ;

A43: cod (F . (f1 (*) f2)) = ((F2 ") * F1) . (cod (f1 (*) f2)) by A33

.= ((F2 ") * F1) . (cod f1) by A40, Th4

.= cod (F . f1) by A33

.= cod ((F . f1) (*) (F . f2)) by A41, Th4 ;

A44: F . (f1 (*) f2) in Hom ((dom (F . (f1 (*) f2))),(cod (F . (f1 (*) f2)))) by Th20;

(F . f1) (*) (F . f2) in Hom ((dom (F . (f1 (*) f2))),(cod (F . (f1 (*) f2)))) by A42, A43, Th20;

hence F . (f1 (*) f2) = (F . f1) (*) (F . f2) by A44, Def12; :: thesis: verum

end;assume A40: f1 |> f2 ; :: thesis: ( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) )

dom (F . f1) = ((F2 ") * F1) . (dom f1) by A33

.= ((F2 ") * F1) . (cod f2) by A2, A40, Th5

.= cod (F . f2) by A33 ;

hence A41: F . f1 |> F . f2 by Th5; :: thesis: F . (f1 (*) f2) = (F . f1) (*) (F . f2)

set g1 = F . (f1 (*) f2);

set g2 = (F . f1) (*) (F . f2);

A42: dom (F . (f1 (*) f2)) = ((F2 ") * F1) . (dom (f1 (*) f2)) by A33

.= ((F2 ") * F1) . (dom f2) by A40, Th4

.= dom (F . f2) by A33

.= dom ((F . f1) (*) (F . f2)) by A41, Th4 ;

A43: cod (F . (f1 (*) f2)) = ((F2 ") * F1) . (cod (f1 (*) f2)) by A33

.= ((F2 ") * F1) . (cod f1) by A40, Th4

.= cod (F . f1) by A33

.= cod ((F . f1) (*) (F . f2)) by A41, Th4 ;

A44: F . (f1 (*) f2) in Hom ((dom (F . (f1 (*) f2))),(cod (F . (f1 (*) f2)))) by Th20;

(F . f1) (*) (F . f2) in Hom ((dom (F . (f1 (*) f2))),(cod (F . (f1 (*) f2)))) by A42, A43, Th20;

hence F . (f1 (*) f2) = (F . f1) (*) (F . f2) by A44, Def12; :: thesis: verum

for f being morphism of C1 st f is identity holds

F . f is identity

proof

then
F is identity-preserving
by CAT_6:def 22;
let f be morphism of C1; :: thesis: ( f is identity implies F . f is identity )

assume A46: f is identity ; :: thesis: F . f is identity

then A47: dom f = f by Th6

.= cod f by A46, Th6 ;

A48: for g1 being morphism of C2 st F . f |> g1 holds

(F . f) (*) g1 = g1

then F . f is right_identity by CAT_6:9;

hence F . f is identity by A48, CAT_6:def 4, CAT_6:def 14; :: thesis: verum

end;assume A46: f is identity ; :: thesis: F . f is identity

then A47: dom f = f by Th6

.= cod f by A46, Th6 ;

A48: for g1 being morphism of C2 st F . f |> g1 holds

(F . f) (*) g1 = g1

proof

then
F . f is left_identity
by CAT_6:def 4;
let g1 be morphism of C2; :: thesis: ( F . f |> g1 implies (F . f) (*) g1 = g1 )

assume A49: F . f |> g1 ; :: thesis: (F . f) (*) g1 = g1

set g2 = (F . f) (*) g1;

A50: dom ((F . f) (*) g1) = dom g1 by A49, Th4;

A51: cod ((F . f) (*) g1) = cod (F . f) by A49, Th4

.= ((F2 ") * F1) . (dom f) by A33, A47

.= dom (F . f) by A33

.= cod g1 by A49, Th5 ;

A52: g1 in Hom ((dom g1),(cod g1)) by A1, A2, Th20;

(F . f) (*) g1 in Hom ((dom g1),(cod g1)) by A50, A51, Th20;

hence (F . f) (*) g1 = g1 by A52, Def12; :: thesis: verum

end;assume A49: F . f |> g1 ; :: thesis: (F . f) (*) g1 = g1

set g2 = (F . f) (*) g1;

A50: dom ((F . f) (*) g1) = dom g1 by A49, Th4;

A51: cod ((F . f) (*) g1) = cod (F . f) by A49, Th4

.= ((F2 ") * F1) . (dom f) by A33, A47

.= dom (F . f) by A33

.= cod g1 by A49, Th5 ;

A52: g1 in Hom ((dom g1),(cod g1)) by A1, A2, Th20;

(F . f) (*) g1 in Hom ((dom g1),(cod g1)) by A50, A51, Th20;

hence (F . f) (*) g1 = g1 by A52, Def12; :: thesis: verum

then F . f is right_identity by CAT_6:9;

hence F . f is identity by A48, CAT_6:def 4, CAT_6:def 14; :: thesis: verum

hence C1 ~= C2 by A32, Th12, A45, CAT_6:def 25, A8, A7, A31; :: thesis: verum

proof

assume
C1 ~= C2
; :: thesis: O1 = O2

then A53: RelOb C1, RelOb C2 are_isomorphic by Th35;

A54: RelOb C1, RelIncl O1 are_isomorphic by Def14;

RelOb C2, RelIncl O2 are_isomorphic by Def14;

then RelOb C1, RelIncl O2 are_isomorphic by A53, WELLORD1:42;

then RelIncl O2, RelOb C1 are_isomorphic by WELLORD1:40;

hence O1 = O2 by A54, WELLORD1:42, WELLORD2:10; :: thesis: verum

end;then A53: RelOb C1, RelOb C2 are_isomorphic by Th35;

A54: RelOb C1, RelIncl O1 are_isomorphic by Def14;

RelOb C2, RelIncl O2 are_isomorphic by Def14;

then RelOb C1, RelIncl O2 are_isomorphic by A53, WELLORD1:42;

then RelIncl O2, RelOb C1 are_isomorphic by WELLORD1:40;

hence O1 = O2 by A54, WELLORD1:42, WELLORD2:10; :: thesis: verum