let A be non empty transitive with_units AltCatStr ; :: thesis: (id A) " = id A

set CCA = [: the carrier of A, the carrier of A:];

consider f being ManySortedFunction of the Arrows of A, the Arrows of A * the ObjectMap of (id A) such that

A1: f = the MorphMap of (id A) and

A2: the MorphMap of ((id A) ") = (f "") * ( the ObjectMap of (id A) ") by FUNCTOR0:def 38;

A3: for i being set st i in [: the carrier of A, the carrier of A:] holds

(id the Arrows of A) . i is one-to-one

then A5: the MorphMap of (id A) is "1-1" by A3, MSUALG_3:1;

for i being set st i in [: the carrier of A, the carrier of A:] holds

rng (f . i) = ( the Arrows of A * the ObjectMap of (id A)) . i

for i being object st i in [: the carrier of A, the carrier of A:] holds

(f "") . i = f . i

for i being object st i in [: the carrier of A, the carrier of A:] holds

( the MorphMap of (id A) * (id [: the carrier of A, the carrier of A:])) . i = the MorphMap of (id A) . i

A13: the ObjectMap of ((id A) ") = the ObjectMap of (id A) " by FUNCTOR0:def 38;

then the ObjectMap of ((id A) ") = (id [: the carrier of A, the carrier of A:]) " by FUNCTOR0:def 29

.= id [: the carrier of A, the carrier of A:] by FUNCT_1:45

.= the ObjectMap of (id A) by FUNCTOR0:def 29 ;

hence (id A) " = id A by A13, A1, A2, A10, A12, FUNCTOR0:def 29; :: thesis: verum

set CCA = [: the carrier of A, the carrier of A:];

consider f being ManySortedFunction of the Arrows of A, the Arrows of A * the ObjectMap of (id A) such that

A1: f = the MorphMap of (id A) and

A2: the MorphMap of ((id A) ") = (f "") * ( the ObjectMap of (id A) ") by FUNCTOR0:def 38;

A3: for i being set st i in [: the carrier of A, the carrier of A:] holds

(id the Arrows of A) . i is one-to-one

proof

the MorphMap of (id A) = id the Arrows of A
by FUNCTOR0:def 29;
let i be set ; :: thesis: ( i in [: the carrier of A, the carrier of A:] implies (id the Arrows of A) . i is one-to-one )

assume A4: i in [: the carrier of A, the carrier of A:] ; :: thesis: (id the Arrows of A) . i is one-to-one

id ( the Arrows of A . i) is one-to-one ;

hence (id the Arrows of A) . i is one-to-one by A4, MSUALG_3:def 1; :: thesis: verum

end;assume A4: i in [: the carrier of A, the carrier of A:] ; :: thesis: (id the Arrows of A) . i is one-to-one

id ( the Arrows of A . i) is one-to-one ;

hence (id the Arrows of A) . i is one-to-one by A4, MSUALG_3:def 1; :: thesis: verum

then A5: the MorphMap of (id A) is "1-1" by A3, MSUALG_3:1;

for i being set st i in [: the carrier of A, the carrier of A:] holds

rng (f . i) = ( the Arrows of A * the ObjectMap of (id A)) . i

proof

then A8:
f is "onto"
;
dom the Arrows of A = [: the carrier of A, the carrier of A:]
by PARTFUN1:def 2;

then A6: (dom the Arrows of A) /\ [: the carrier of A, the carrier of A:] = [: the carrier of A, the carrier of A:] ;

let i be set ; :: thesis: ( i in [: the carrier of A, the carrier of A:] implies rng (f . i) = ( the Arrows of A * the ObjectMap of (id A)) . i )

assume A7: i in [: the carrier of A, the carrier of A:] ; :: thesis: rng (f . i) = ( the Arrows of A * the ObjectMap of (id A)) . i

rng (f . i) = rng ((id the Arrows of A) . i) by A1, FUNCTOR0:def 29

.= rng (id ( the Arrows of A . i)) by A7, MSUALG_3:def 1

.= the Arrows of A . i

.= ( the Arrows of A * (id [: the carrier of A, the carrier of A:])) . i by A7, A6, FUNCT_1:20

.= ( the Arrows of A * the ObjectMap of (id A)) . i by FUNCTOR0:def 29 ;

hence rng (f . i) = ( the Arrows of A * the ObjectMap of (id A)) . i ; :: thesis: verum

end;then A6: (dom the Arrows of A) /\ [: the carrier of A, the carrier of A:] = [: the carrier of A, the carrier of A:] ;

let i be set ; :: thesis: ( i in [: the carrier of A, the carrier of A:] implies rng (f . i) = ( the Arrows of A * the ObjectMap of (id A)) . i )

assume A7: i in [: the carrier of A, the carrier of A:] ; :: thesis: rng (f . i) = ( the Arrows of A * the ObjectMap of (id A)) . i

rng (f . i) = rng ((id the Arrows of A) . i) by A1, FUNCTOR0:def 29

.= rng (id ( the Arrows of A . i)) by A7, MSUALG_3:def 1

.= the Arrows of A . i

.= ( the Arrows of A * (id [: the carrier of A, the carrier of A:])) . i by A7, A6, FUNCT_1:20

.= ( the Arrows of A * the ObjectMap of (id A)) . i by FUNCTOR0:def 29 ;

hence rng (f . i) = ( the Arrows of A * the ObjectMap of (id A)) . i ; :: thesis: verum

for i being object st i in [: the carrier of A, the carrier of A:] holds

(f "") . i = f . i

proof

then A10:
f "" = f
;
let i be object ; :: thesis: ( i in [: the carrier of A, the carrier of A:] implies (f "") . i = f . i )

assume A9: i in [: the carrier of A, the carrier of A:] ; :: thesis: (f "") . i = f . i

then (f "") . i = ( the MorphMap of (id A) . i) " by A1, A5, A8, MSUALG_3:def 4

.= ((id the Arrows of A) . i) " by FUNCTOR0:def 29

.= (id ( the Arrows of A . i)) " by A9, MSUALG_3:def 1

.= id ( the Arrows of A . i) by FUNCT_1:45

.= (id the Arrows of A) . i by A9, MSUALG_3:def 1

.= f . i by A1, FUNCTOR0:def 29 ;

hence (f "") . i = f . i ; :: thesis: verum

end;assume A9: i in [: the carrier of A, the carrier of A:] ; :: thesis: (f "") . i = f . i

then (f "") . i = ( the MorphMap of (id A) . i) " by A1, A5, A8, MSUALG_3:def 4

.= ((id the Arrows of A) . i) " by FUNCTOR0:def 29

.= (id ( the Arrows of A . i)) " by A9, MSUALG_3:def 1

.= id ( the Arrows of A . i) by FUNCT_1:45

.= (id the Arrows of A) . i by A9, MSUALG_3:def 1

.= f . i by A1, FUNCTOR0:def 29 ;

hence (f "") . i = f . i ; :: thesis: verum

for i being object st i in [: the carrier of A, the carrier of A:] holds

( the MorphMap of (id A) * (id [: the carrier of A, the carrier of A:])) . i = the MorphMap of (id A) . i

proof

then A12:
the MorphMap of (id A) * (id [: the carrier of A, the carrier of A:]) = the MorphMap of (id A)
;
dom the MorphMap of (id A) = [: the carrier of A, the carrier of A:]
by PARTFUN1:def 2;

then A11: (dom the MorphMap of (id A)) /\ [: the carrier of A, the carrier of A:] = [: the carrier of A, the carrier of A:] ;

let i be object ; :: thesis: ( i in [: the carrier of A, the carrier of A:] implies ( the MorphMap of (id A) * (id [: the carrier of A, the carrier of A:])) . i = the MorphMap of (id A) . i )

assume i in [: the carrier of A, the carrier of A:] ; :: thesis: ( the MorphMap of (id A) * (id [: the carrier of A, the carrier of A:])) . i = the MorphMap of (id A) . i

hence ( the MorphMap of (id A) * (id [: the carrier of A, the carrier of A:])) . i = the MorphMap of (id A) . i by A11, FUNCT_1:20; :: thesis: verum

end;then A11: (dom the MorphMap of (id A)) /\ [: the carrier of A, the carrier of A:] = [: the carrier of A, the carrier of A:] ;

let i be object ; :: thesis: ( i in [: the carrier of A, the carrier of A:] implies ( the MorphMap of (id A) * (id [: the carrier of A, the carrier of A:])) . i = the MorphMap of (id A) . i )

assume i in [: the carrier of A, the carrier of A:] ; :: thesis: ( the MorphMap of (id A) * (id [: the carrier of A, the carrier of A:])) . i = the MorphMap of (id A) . i

hence ( the MorphMap of (id A) * (id [: the carrier of A, the carrier of A:])) . i = the MorphMap of (id A) . i by A11, FUNCT_1:20; :: thesis: verum

A13: the ObjectMap of ((id A) ") = the ObjectMap of (id A) " by FUNCTOR0:def 38;

then the ObjectMap of ((id A) ") = (id [: the carrier of A, the carrier of A:]) " by FUNCTOR0:def 29

.= id [: the carrier of A, the carrier of A:] by FUNCT_1:45

.= the ObjectMap of (id A) by FUNCTOR0:def 29 ;

hence (id A) " = id A by A13, A1, A2, A10, A12, FUNCTOR0:def 29; :: thesis: verum