:: ALTCAT_4 semantic presentation
theorem E1: :: ALTCAT_4:1
proof
let c
1 be
category;
let c
2, c
3, c
4 be
object of c
1;
let c
5 be
Morphism of c
2,c
3;
let c
6 be
Morphism of c
2,c
4;
let c
7 be
Morphism of c
3,c
4;
assume that
E2:
c
6 = c
7 * c
5
and
E3:
(c7 " ) * c
7 = idm c
3
and
E4:
(
<^c2,c3^> <> {} &
<^c3,c4^> <> {} &
<^c4,c3^> <> {} )
;
thus (c7 " ) * c
6 =
((c7 " ) * c7) * c
5
by E2, E4, ALTCAT_1:25
.=
c
5
by E3, E4, ALTCAT_1:24
;
end;
theorem E2: :: ALTCAT_4:2
proof
let c
1 be
category;
let c
2, c
3, c
4 be
object of c
1;
let c
5 be
Morphism of c
2,c
3;
let c
6 be
Morphism of c
4,c
3;
let c
7 be
Morphism of c
4,c
2;
assume that
E3:
c
6 = c
5 * c
7
and
E4:
c
7 * (c7 " ) = idm c
2
and
E5:
(
<^c4,c2^> <> {} &
<^c2,c4^> <> {} &
<^c2,c3^> <> {} )
;
thus c
6 * (c7 " ) =
c
5 * (c7 * (c7 " ))
by E3, E5, ALTCAT_1:25
.=
c
5
by E4, E5, ALTCAT_1:def 19
;
end;
theorem E3: :: ALTCAT_4:3
proof
let c
1 be
category;
let c
2, c
3 be
object of c
1;
let c
4 be
Morphism of c
2,c
3;
assume E4:
(
<^c2,c3^> <> {} &
<^c3,c2^> <> {} )
;
assume
c
4 is
iso
;
then E5:
( c
4 is
retraction & c
4 is
coretraction )
by ALTCAT_3:5;
hence (c4 " ) * ((c4 " ) " ) =
(c4 " ) * c
4
by E4, ALTCAT_3:3
.=
idm c
2
by E4, E5, ALTCAT_3:2
;
:: uses ALTCAT_3:def 5
thus ((c4 " ) " ) * (c4 " ) =
c
4 * (c4 " )
by E4, E5, ALTCAT_3:3
.=
idm c
3
by E4, E5, ALTCAT_3:2
;
end;
theorem E4: :: ALTCAT_4:4
theorem :: ALTCAT_4:5
proof
let c
1 be
category;
let c
2, c
3 be
object of c
1;
let c
4 be
Morphism of c
2,c
3;
let c
5, c
6 be
Morphism of c
3,c
2;
assume that
E5:
c
6 * c
4 = idm c
2
and
E6:
c
4 * c
5 = idm c
3
and
E7:
(
<^c2,c3^> <> {} &
<^c3,c2^> <> {} )
;
thus c
5 =
(c6 * c4) * c
5
by E5, E7, ALTCAT_1:24
.=
c
6 * (idm c3)
by E6, E7, ALTCAT_1:25
.=
c
6
by E7, ALTCAT_1:def 19
;
end;
theorem :: ALTCAT_4:6
theorem :: ALTCAT_4:7
proof
let c
1 be
category;
let c
2, c
3 be
object of c
1;
let c
4, c
5 be
Morphism of c
2,c
3;
assume that
E5:
c
4 is
_zero
and
E6:
c
5 is
_zero
;
given c
6 being
object of c
1 such that
E7:
c
6 is
_zero
;
consider c
7 being
Morphism of c
2,c
6;
consider c
8 being
Morphism of c
6,c
3;
consider c
9 being
Morphism of c
6,c
6;
thus c
4 =
(c8 * ((c9 " ) * c9)) * c
7
by E5, E7, ALTCAT_3:def 12
.=
c
5
by E6, E7, ALTCAT_3:def 12
;
end;
theorem :: ALTCAT_4:8
proof
let c
1 be non
empty AltCatStr ;
let c
2, c
3 be
object of c
1;
let c
4 be
Morphism of c
2,c
3;
assume E5:
c
2 is
terminal
;
let c
5 be
object of c
1;
:: uses ALTCAT_3:def 7
assume E6:
<^c5,c2^> <> {}
;
let c
6, c
7 be
Morphism of c
5,c
2;
assume
c
4 * c
6 = c
4 * c
7
;
consider c
8 being
Morphism of c
5,c
2 such that
c
8 in <^c5,c2^>
and
E7:
for b
1 being
Morphism of c
5,c
2 holds
( b
1 in <^c5,c2^> implies c
8 = b
1 )
by E5, ALTCAT_3:27;
thus c
6 =
c
8
by E6, E7
.=
c
7
by E6, E7
;
end;
theorem :: ALTCAT_4:9
proof
let c
1 be non
empty AltCatStr ;
let c
2, c
3 be
object of c
1;
let c
4 be
Morphism of c
3,c
2;
assume E5:
c
2 is
initial
;
let c
5 be
object of c
1;
:: uses ALTCAT_3:def 8
assume E6:
<^c2,c5^> <> {}
;
let c
6, c
7 be
Morphism of c
2,c
5;
assume
c
6 * c
4 = c
7 * c
4
;
consider c
8 being
Morphism of c
2,c
5 such that
c
8 in <^c2,c5^>
and
E7:
for b
1 being
Morphism of c
2,c
5 holds
( b
1 in <^c2,c5^> implies c
8 = b
1 )
by E5, ALTCAT_3:25;
thus c
6 =
c
8
by E6, E7
.=
c
7
by E6, E7
;
end;
theorem :: ALTCAT_4:10
proof
let c
1 be
category;
let c
2, c
3 be
object of c
1;
assume that
E5:
c
2 is
terminal
and
E6:
c
3,c
2 are_iso
;
for b
1 being
object of c
1 holds
ex b
2 being
Morphism of b
1,c
3 st
( b
2 in <^b1,c3^> & for b
3 being
Morphism of b
1,c
3 holds
( b
3 in <^b1,c3^> implies b
2 = b
3 ) )
proof
let c
4 be
object of c
1;
consider c
5 being
Morphism of c
4,c
2 such that
E7:
c
5 in <^c4,c2^>
and
E8:
for b
1 being
Morphism of c
4,c
2 holds
( b
1 in <^c4,c2^> implies c
5 = b
1 )
by E5, ALTCAT_3:27;
consider c
6 being
Morphism of c
3,c
2 such that
E9:
c
6 is
iso
by E6, ALTCAT_3:def 6;
E10:
(c6 " ) * c
6 = idm c
3
by E9, ALTCAT_3:def 5;
take
(c6 " ) * c
5
;
E11:
(
<^c3,c2^> <> {} &
<^c2,c3^> <> {} )
by E6, ALTCAT_3:def 6;
then E12:
<^c4,c3^> <> {}
by E7, ALTCAT_1:def 4;
hence
(c6 " ) * c
5 in <^c4,c3^>
;
let c
7 be
Morphism of c
4,c
3;
assume
c
7 in <^c4,c3^>
;
c
6 * c
7 = c
5
by E7, E8;
hence
(c6 " ) * c
5 = c
7
by E10, E11, E12, E1;
end;
hence
c
3 is
terminal
by ALTCAT_3:27;
end;
theorem :: ALTCAT_4:11
proof
let c
1 be
category;
let c
2, c
3 be
object of c
1;
assume that
E5:
c
2 is
initial
and
E6:
c
2,c
3 are_iso
;
for b
1 being
object of c
1 holds
ex b
2 being
Morphism of c
3,b
1 st
( b
2 in <^c3,b1^> & for b
3 being
Morphism of c
3,b
1 holds
( b
3 in <^c3,b1^> implies b
2 = b
3 ) )
proof
let c
4 be
object of c
1;
consider c
5 being
Morphism of c
2,c
4 such that
E7:
c
5 in <^c2,c4^>
and
E8:
for b
1 being
Morphism of c
2,c
4 holds
( b
1 in <^c2,c4^> implies c
5 = b
1 )
by E5, ALTCAT_3:25;
consider c
6 being
Morphism of c
2,c
3 such that
E9:
c
6 is
iso
by E6, ALTCAT_3:def 6;
E10:
c
6 * (c6 " ) = idm c
3
by E9, ALTCAT_3:def 5;
take
c
5 * (c6 " )
;
E11:
(
<^c2,c3^> <> {} &
<^c3,c2^> <> {} )
by E6, ALTCAT_3:def 6;
then E12:
<^c3,c4^> <> {}
by E7, ALTCAT_1:def 4;
hence
c
5 * (c6 " ) in <^c3,c4^>
;
let c
7 be
Morphism of c
3,c
4;
assume
c
7 in <^c3,c4^>
;
c
7 * c
6 = c
5
by E7, E8;
hence
c
5 * (c6 " ) = c
7
by E10, E11, E12, E2;
end;
hence
c
3 is
initial
by ALTCAT_3:25;
end;
theorem :: ALTCAT_4:12
proof
let c
1 be
category;
let c
2, c
3 be
object of c
1;
assume that
E5:
c
2 is
initial
and
E6:
c
3 is
terminal
;
assume
<^c3,c2^> <> {}
;
then consider c
4 being
set such that
E7:
c
4 in <^c3,c2^>
by XBOOLE_0:def 1;
reconsider c
5 = c
4 as
Morphism of c
3,c
2 by E7;
consider c
6 being
Morphism of c
2,c
3 such that
E8:
c
6 in <^c2,c3^>
and
for b
1 being
Morphism of c
2,c
3 holds
( b
1 in <^c2,c3^> implies c
6 = b
1 )
by E5, ALTCAT_3:25;
for b
1 being
object of c
1 holds
ex b
2 being
Morphism of c
3,b
1 st
( b
2 in <^c3,b1^> & for b
3 being
Morphism of c
3,b
1 holds
( b
3 in <^c3,b1^> implies b
2 = b
3 ) )
proof
let c
7 be
object of c
1;
consider c
8 being
Morphism of c
2,c
7 such that
E9:
( c
8 in <^c2,c7^> & for b
1 being
Morphism of c
2,c
7 holds
( b
1 in <^c2,c7^> implies c
8 = b
1 ) )
by E5, ALTCAT_3:25;
take
c
8 * c
5
;
<^c3,c7^> <> {}
by E7, E9, ALTCAT_1:def 4;
hence
c
8 * c
5 in <^c3,c7^>
;
let c
9 be
Morphism of c
3,c
7;
assume E10:
c
9 in <^c3,c7^>
;
consider c
10 being
Morphism of c
3,c
3 such that
c
10 in <^c3,c3^>
and
E11:
for b
1 being
Morphism of c
3,c
3 holds
( b
1 in <^c3,c3^> implies c
10 = b
1 )
by E6, ALTCAT_3:27;
thus c
8 * c
5 =
(c9 * c6) * c
5
by E9
.=
c
9 * (c6 * c5)
by E7, E8, E10, ALTCAT_1:25
.=
c
9 * c
10
by E11
.=
c
9 * (idm c3)
by E11
.=
c
9
by E10, ALTCAT_1:def 19
;
end;
hence
c
3 is
initial
by ALTCAT_3:25;
for b
1 being
object of c
1 holds
ex b
2 being
Morphism of b
1,c
2 st
( b
2 in <^b1,c2^> & for b
3 being
Morphism of b
1,c
2 holds
( b
3 in <^b1,c2^> implies b
2 = b
3 ) )
proof
let c
7 be
object of c
1;
consider c
8 being
Morphism of c
7,c
3 such that
E9:
( c
8 in <^c7,c3^> & for b
1 being
Morphism of c
7,c
3 holds
( b
1 in <^c7,c3^> implies c
8 = b
1 ) )
by E6, ALTCAT_3:27;
take
c
5 * c
8
;
<^c7,c2^> <> {}
by E7, E9, ALTCAT_1:def 4;
hence
c
5 * c
8 in <^c7,c2^>
;
let c
9 be
Morphism of c
7,c
2;
assume E10:
c
9 in <^c7,c2^>
;
consider c
10 being
Morphism of c
2,c
2 such that
c
10 in <^c2,c2^>
and
E11:
for b
1 being
Morphism of c
2,c
2 holds
( b
1 in <^c2,c2^> implies c
10 = b
1 )
by E5, ALTCAT_3:25;
thus c
5 * c
8 =
c
5 * (c6 * c9)
by E9
.=
(c5 * c6) * c
9
by E7, E8, E10, ALTCAT_1:25
.=
c
10 * c
9
by E11
.=
(idm c2) * c
9
by E11
.=
c
9
by E10, ALTCAT_1:24
;
end;
hence
c
2 is
terminal
by ALTCAT_3:27;
end;
theorem E5: :: ALTCAT_4:13
theorem E6: :: ALTCAT_4:14
proof
let c
1, c
2 be non
empty AltCatStr ;
let c
3 be
Contravariant FunctorStr of c
1,c
2;
set c
4 =
[:the carrier of c1,the carrier of c1:];
hereby
assume E7:
c
3 is
full
;
let c
5, c
6 be
object of c
1;
thus
Morph-Map c
3,c
6,c
5 is
onto
proof
consider c
7 being
ManySortedFunction of the
Arrows of c
1,the
Arrows of c
2 * the
ObjectMap of c
3 such that
E8:
( c
7 = the
MorphMap of c
3 & c
7 is
"onto" )
by E7, FUNCTOR0:def 33;
E9:
[c6,c5] in [:the carrier of c1,the carrier of c1:]
by ZFMISC_1:106;
E10:
the
MorphMap of c
3 . [c6,c5] = the
MorphMap of c
3 . c
6,c
5
by BINOP_1:def 1;
E11:
[c6,c5] in dom the
ObjectMap of c
3
by E9, FUNCT_2:def 1;
rng (c7 . [c6,c5]) = (the Arrows of c2 * the ObjectMap of c3) . [c6,c5]
by E8, E9, MSUALG_3:def 3;
hence rng (Morph-Map c3,c6,c5) =
(the Arrows of c2 * the ObjectMap of c3) . [c6,c5]
by E8, E10
.=
the
Arrows of c
2 . (the ObjectMap of c3 . [c6,c5])
by E11, FUNCT_1:23
.=
the
Arrows of c
2 . (the ObjectMap of c3 . c6,c5)
by BINOP_1:def 1
.=
the
Arrows of c
2 . [(c3 . c5),(c3 . c6)]
by FUNCTOR0:24
.=
the
Arrows of c
2 . (c3 . c5),
(c3 . c6)
by BINOP_1:def 1
.=
<^(c3 . c5),(c3 . c6)^>
;
:: uses FUNCT_2:def 3
end;
end;
assume E7:
for b
1, b
2 being
object of c
1 holds
Morph-Map c
3,b
2,b
1 is
onto
;
consider c
5 being non
empty set , c
6 being
ManySortedSet of c
5, c
7 being
Function of
[:the carrier of c1,the carrier of c1:],c
5 such that
E8:
the
ObjectMap of c
3 = c
7
and
E9:
( the
Arrows of c
2 = c
6 & the
MorphMap of c
3 is
ManySortedFunction of the
Arrows of c
1,c
6 * c
7 )
by FUNCTOR0:def 4;
reconsider c
8 = the
MorphMap of c
3 as
ManySortedFunction of the
Arrows of c
1,the
Arrows of c
2 * the
ObjectMap of c
3 by E8, E9;
take
c
8
;
:: uses FUNCTOR0:def 33
thus
c
8 = the
MorphMap of c
3
;
let c
9 be
set ;
:: uses MSUALG_3:def 3
assume
c
9 in [:the carrier of c1,the carrier of c1:]
;
then consider c
10, c
11 being
set such that
E10:
( c
10 in the
carrier of c
1 & c
11 in the
carrier of c
1 & c
9 = [c10,c11] )
by ZFMISC_1:103;
reconsider c
12 = c
11, c
13 = c
10 as
object of c
1 by E10;
E11:
[c13,c12] in [:the carrier of c1,the carrier of c1:]
by ZFMISC_1:106;
E12:
the
MorphMap of c
3 . [c13,c12] = the
MorphMap of c
3 . c
13,c
12
by BINOP_1:def 1;
E13:
[c13,c12] in dom the
ObjectMap of c
3
by E11, FUNCT_2:def 1;
Morph-Map c
3,c
13,c
12 is
onto
by E7;
then rng (Morph-Map c3,c13,c12) =
<^(c3 . c12),(c3 . c13)^>
by FUNCT_2:def 3
.=
the
Arrows of c
2 . (c3 . c12),
(c3 . c13)
.=
the
Arrows of c
2 . [(c3 . c12),(c3 . c13)]
by BINOP_1:def 1
.=
the
Arrows of c
2 . (the ObjectMap of c3 . c13,c12)
by FUNCTOR0:24
.=
the
Arrows of c
2 . (the ObjectMap of c3 . [c13,c12])
by BINOP_1:def 1
.=
(the Arrows of c2 * the ObjectMap of c3) . [c13,c12]
by E13, FUNCT_1:23
;
hence
rng (c8 . c9) = (the Arrows of c2 * the ObjectMap of c3) . c
9
by E10, E12;
end;
theorem E7: :: ALTCAT_4:15
proof
let c
1, c
2 be non
empty AltCatStr ;
let c
3 be
Contravariant FunctorStr of c
1,c
2;
set c
4 =
[:the carrier of c1,the carrier of c1:];
hereby
assume E8:
c
3 is
faithful
;
let c
5, c
6 be
object of c
1;
E9:
the
MorphMap of c
3 is
"1-1"
by E8, FUNCTOR0:def 31;
E10:
[c6,c5] in [:the carrier of c1,the carrier of c1:]
by ZFMISC_1:106;
E11:
the
MorphMap of c
3 . [c6,c5] = the
MorphMap of c
3 . c
6,c
5
by BINOP_1:def 1;
reconsider c
7 = the
MorphMap of c
3 . [c6,c5] as
Function ;
dom the
MorphMap of c
3 = [:the carrier of c1,the carrier of c1:]
by PBOOLE:def 3;
then
c
7 is
one-to-one
by E9, E10, MSUALG_3:def 2;
hence
Morph-Map c
3,c
6,c
5 is
one-to-one
by E11;
end;
assume E8:
for b
1, b
2 being
object of c
1 holds
Morph-Map c
3,b
2,b
1 is
one-to-one
;
let c
5 be
set ;
:: uses FUNCTOR0:def 31,
MSUALG_3:def 2let c
6 be
Function;
assume E9:
( c
5 in dom the
MorphMap of c
3 & the
MorphMap of c
3 . c
5 = c
6 )
;
dom the
MorphMap of c
3 = [:the carrier of c1,the carrier of c1:]
by PBOOLE:def 3;
then consider c
7, c
8 being
set such that
E10:
( c
7 in the
carrier of c
1 & c
8 in the
carrier of c
1 & c
5 = [c7,c8] )
by E9, ZFMISC_1:103;
reconsider c
9 = c
7, c
10 = c
8 as
object of c
1 by E10;
E11:
the
MorphMap of c
3 . c
9,c
10 = Morph-Map c
3,c
9,c
10
;
the
MorphMap of c
3 . [c9,c10] = the
MorphMap of c
3 . c
9,c
10
by BINOP_1:def 1;
hence
c
6 is
one-to-one
by E8, E9, E10, E11;
end;
theorem E8: :: ALTCAT_4:16
proof
let c
1, c
2 be non
empty AltCatStr ;
let c
3 be
Covariant FunctorStr of c
1,c
2;
let c
4, c
5 be
object of c
1;
let c
6 be
Morphism of
(c3 . c4),
(c3 . c5);
assume E9:
<^c4,c5^> <> {}
;
assume
c
3 is
full
;
then
Morph-Map c
3,c
4,c
5 is
onto
by FUNCTOR1:18;
then E10:
rng (Morph-Map c3,c4,c5) = <^(c3 . c4),(c3 . c5)^>
by FUNCT_2:def 3;
assume
c
3 is
feasible
;
then E11:
<^(c3 . c4),(c3 . c5)^> <> {}
by E9, FUNCTOR0:def 19;
then consider c
7 being
set such that
E12:
c
7 in dom (Morph-Map c3,c4,c5)
and
E13:
c
6 = (Morph-Map c3,c4,c5) . c
7
by E10, FUNCT_1:def 5;
reconsider c
8 = c
7 as
Morphism of c
4,c
5 by E11, E12, FUNCT_2:def 1;
take
c
8
;
thus
c
6 = c
3 . c
8
by E9, E11, E13, FUNCTOR0:def 16;
end;
theorem E9: :: ALTCAT_4:17
proof
let c
1, c
2 be non
empty AltCatStr ;
let c
3 be
Contravariant FunctorStr of c
1,c
2;
let c
4, c
5 be
object of c
1;
let c
6 be
Morphism of
(c3 . c5),
(c3 . c4);
assume E10:
<^c4,c5^> <> {}
;
assume
c
3 is
full
;
then
Morph-Map c
3,c
4,c
5 is
onto
by E6;
then E11:
rng (Morph-Map c3,c4,c5) = <^(c3 . c5),(c3 . c4)^>
by FUNCT_2:def 3;
assume
c
3 is
feasible
;
then E12:
<^(c3 . c5),(c3 . c4)^> <> {}
by E10, FUNCTOR0:def 20;
then consider c
7 being
set such that
E13:
c
7 in dom (Morph-Map c3,c4,c5)
and
E14:
c
6 = (Morph-Map c3,c4,c5) . c
7
by E11, FUNCT_1:def 5;
reconsider c
8 = c
7 as
Morphism of c
4,c
5 by E12, E13, FUNCT_2:def 1;
take
c
8
;
thus
c
6 = c
3 . c
8
by E10, E12, E14, FUNCTOR0:def 17;
end;
theorem E10: :: ALTCAT_4:18
theorem E11: :: ALTCAT_4:19
theorem E12: :: ALTCAT_4:20
proof
let c
1, c
2 be
category;
let c
3 be
covariant Functor of c
1,c
2;
let c
4, c
5 be
object of c
1;
let c
6 be
Morphism of c
4,c
5;
assume that
E13:
(
<^c4,c5^> <> {} &
<^c5,c4^> <> {} )
and
E14:
c
6 is
iso
;
E15:
(
<^(c3 . c4),(c3 . c5)^> <> {} &
<^(c3 . c5),(c3 . c4)^> <> {} )
by E13, FUNCTOR0:def 19;
( c
6 is
retraction & c
6 is
coretraction )
by E13, E14, ALTCAT_3:6;
then
( c
3 . c
6 is
retraction & c
3 . c
6 is
coretraction )
by E13, E10, E11;
hence
c
3 . c
6 is
iso
by E15, ALTCAT_3:6;
end;
theorem :: ALTCAT_4:21
proof
let c
1, c
2 be
category;
let c
3 be
covariant Functor of c
1,c
2;
let c
4, c
5 be
object of c
1;
assume E13:
c
4,c
5 are_iso
;
then E14:
(
<^c4,c5^> <> {} &
<^c5,c4^> <> {} )
by ALTCAT_3:def 6;
hence
(
<^(c3 . c4),(c3 . c5)^> <> {} &
<^(c3 . c5),(c3 . c4)^> <> {} )
by FUNCTOR0:def 19;
:: uses ALTCAT_3:def 6
consider c
6 being
Morphism of c
4,c
5 such that
E15:
c
6 is
iso
by E13, ALTCAT_3:def 6;
take
c
3 . c
6
;
thus
c
3 . c
6 is
iso
by E14, E15, E12;
end;
theorem E13: :: ALTCAT_4:22
theorem E14: :: ALTCAT_4:23
theorem E15: :: ALTCAT_4:24
proof
let c
1, c
2 be
category;
let c
3 be
contravariant Functor of c
1,c
2;
let c
4, c
5 be
object of c
1;
let c
6 be
Morphism of c
4,c
5;
assume that
E16:
(
<^c4,c5^> <> {} &
<^c5,c4^> <> {} )
and
E17:
c
6 is
iso
;
E18:
(
<^(c3 . c4),(c3 . c5)^> <> {} &
<^(c3 . c5),(c3 . c4)^> <> {} )
by E16, FUNCTOR0:def 20;
( c
6 is
retraction & c
6 is
coretraction )
by E16, E17, ALTCAT_3:6;
then
( c
3 . c
6 is
retraction & c
3 . c
6 is
coretraction )
by E16, E13, E14;
hence
c
3 . c
6 is
iso
by E18, ALTCAT_3:6;
end;
theorem :: ALTCAT_4:25
proof
let c
1, c
2 be
category;
let c
3 be
contravariant Functor of c
1,c
2;
let c
4, c
5 be
object of c
1;
assume E16:
c
4,c
5 are_iso
;
then E17:
(
<^c4,c5^> <> {} &
<^c5,c4^> <> {} )
by ALTCAT_3:def 6;
hence
(
<^(c3 . c5),(c3 . c4)^> <> {} &
<^(c3 . c4),(c3 . c5)^> <> {} )
by FUNCTOR0:def 20;
:: uses ALTCAT_3:def 6
consider c
6 being
Morphism of c
4,c
5 such that
E18:
c
6 is
iso
by E16, ALTCAT_3:def 6;
take
c
3 . c
6
;
thus
c
3 . c
6 is
iso
by E17, E18, E15;
end;
theorem E16: :: ALTCAT_4:26