let o1, o2, m1, m2 be object ; :: thesis: 1Cat (o1,m1) ~= 1Cat (o2,m2)
set C = 1Cat (o1,m1);
set C9 = 1Cat (o2,m2);
A1: 1Cat (o1,m1) = CatStr(# {o1},{m1},(m1 :-> o1),(m1 :-> o1),((m1,m1) :-> m1) #) by CAT_1:def 11;
A2: 1Cat (o2,m2) = CatStr(# {o2},{m2},(m2 :-> o2),(m2 :-> o2),((m2,m2) :-> m2) #) by CAT_1:def 11;
reconsider o19 = o1 as Element of (1Cat (o1,m1)) by A1, TARSKI:def 1;
reconsider o29 = o2 as Element of (1Cat (o2,m2)) by A2, TARSKI:def 1;
reconsider m19 = m1 as Element of the carrier' of (1Cat (o1,m1)) by A1, TARSKI:def 1;
reconsider m29 = m2 as Element of the carrier' of (1Cat (o2,m2)) by A2, TARSKI:def 1;
set F = m1 :-> m2;
reconsider F = m1 :-> m2 as Function of the carrier' of (1Cat (o1,m1)), the carrier' of (1Cat (o2,m2)) by A1, A2;

now :: thesis: ( ( for c being Element of (1Cat (o1,m1)) ex d being Element of (1Cat (o2,m2)) st F . (id c) = id d ) & ( for f being Element of the carrier' of (1Cat (o1,m1)) holds
( F . (id (dom f)) = id (dom (F . f)) & F . (id (cod f)) = id (cod (F . f)) ) ) & ( for f, g being Element of the carrier' of (1Cat (o1,m1)) st [g,f] in dom the Comp of (1Cat (o1,m1)) holds
F . (g (*) f) = (F . g) (*) (F . f) ) )

hereby :: thesis: ( ( for f being Element of the carrier' of (1Cat (o1,m1)) holds
( F . (id (dom f)) = id (dom (F . f)) & F . (id (cod f)) = id (cod (F . f)) ) ) & ( for f, g being Element of the carrier' of (1Cat (o1,m1)) st [g,f] in dom the Comp of (1Cat (o1,m1)) holds
F . (g (*) f) = (F . g) (*) (F . f) ) )

let c be Element of (1Cat (o1,m1)); :: thesis: ex d being Element of (1Cat (o2,m2)) st F . (id c) = id d
A3: F . (id c) = F . m1 by Th59
.= m2 by FUNCOP_1:72 ;
reconsider c9 = o2 as Element of (1Cat (o2,m2)) by TARSKI:def 1, A2;
id c9 = m2 by Th59;
hence ex d being Element of (1Cat (o2,m2)) st F . (id c) = id d by A3; :: thesis: verum

end;

hereby :: thesis: for f, g being Element of the carrier' of (1Cat (o1,m1)) st [g,f] in dom the Comp of (1Cat (o1,m1)) holds
F . (g (*) f) = (F . g) (*) (F . f)

let f be Element of the carrier' of (1Cat (o1,m1)); :: thesis: ( F . (id (dom f)) = id (dom (F . f)) & F . (id (cod f)) = id (cod (F . f)) )
thus F . (id (dom f)) = F . m1 by Th59
.= m2 by FUNCOP_1:72
.= id (dom (F . f)) by Th59 ; :: thesis: F . (id (cod f)) = id (cod (F . f))
thus F . (id (cod f)) = F . m1 by Th59
.= m2 by FUNCOP_1:72
.= id (cod (F . f)) by Th59 ; :: thesis: verum

end;

thus for f, g being Element of the carrier' of (1Cat (o1,m1)) st [g,f] in dom the Comp of (1Cat (o1,m1)) holds
F . (g (*) f) = (F . g) (*) (F . f) by A1, A2, TARSKI:def 1; :: thesis: verum

end;

then reconsider F = F as Functor of 1Cat (o1,m1), 1Cat (o2,m2) by CAT_1:def 21;

now :: thesis: ( F is one-to-one & rng F = the carrier' of (1Cat (o2,m2)) & rng (Obj F) = the carrier of (1Cat (o2,m2)) )

thus F is one-to-one ; :: thesis: ( rng F = the carrier' of (1Cat (o2,m2)) & rng (Obj F) = the carrier of (1Cat (o2,m2)) )
thus rng F = the carrier' of (1Cat (o2,m2)) by A2; :: thesis: rng (Obj F) = the carrier of (1Cat (o2,m2))
A4: for c being Element of (1Cat (o1,m1)) ex c9 being Element of (1Cat (o2,m2)) st F . (id c) = id c9

proof

let c be Element of (1Cat (o1,m1)); :: thesis: ex c9 being Element of (1Cat (o2,m2)) st F . (id c) = id c9
A5: F . (id c) = F . m1 by Th59
.= m2 by FUNCOP_1:72 ;
reconsider c9 = o2 as Element of (1Cat (o2,m2)) by A2, TARSKI:def 1;
id c9 = m2 by Th59;
hence ex c9 being Element of (1Cat (o2,m2)) st F . (id c) = id c9 by A5; :: thesis: verum

end;

reconsider o19 = o1 as Element of (1Cat (o1,m1)) by A1, TARSKI:def 1;
reconsider o29 = o2 as Element of (1Cat (o2,m2)) by A2, TARSKI:def 1;
A6: F . (id o19) = F . m1 by Th59
.= m2 by FUNCOP_1:72
.= id o29 by Th59 ;
dom (Obj F) = {o1} by A1, PARTFUN1:def 2;
then rng (Obj F) = {((Obj F) . o19)} by FUNCT_1:4
.= {o29} by A6, A4, CAT_1:def 22 ;
hence rng (Obj F) = the carrier of (1Cat (o2,m2)) by A2; :: thesis: verum

end;

hence 1Cat (o1,m1) ~= 1Cat (o2,m2) by CAT_1:def 25, ISOCAT_1:def 4; :: thesis: verum