let D be non empty SubCatStr of C; ( D is transitive implies D is associative )
assume
D is transitive
; D is associative
then reconsider D = D as non empty transitive SubCatStr of C ;
D is associative
proof
let o1,
o2,
o3,
o4 be
object of
D;
ALTCAT_2:def 8 for f being Morphism of o1,o2
for g being Morphism of o2,o3
for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds
(h * g) * f = h * (g * f)
A1:
(
o1 in the
carrier of
D &
o2 in the
carrier of
D )
;
A2:
(
o3 in the
carrier of
D &
o4 in the
carrier of
D )
;
the
carrier of
D c= the
carrier of
C
by Def11;
then reconsider p1 =
o1,
p2 =
o2,
p3 =
o3,
p4 =
o4 as
object of
C by A1, A2;
let f be
Morphism of
o1,
o2;
for g being Morphism of o2,o3
for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds
(h * g) * f = h * (g * f)let g be
Morphism of
o2,
o3;
for h being Morphism of o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds
(h * g) * f = h * (g * f)let h be
Morphism of
o3,
o4;
( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} implies (h * g) * f = h * (g * f) )
assume that A3:
<^o1,o2^> <> {}
and A4:
<^o2,o3^> <> {}
and A5:
<^o3,o4^> <> {}
;
(h * g) * f = h * (g * f)
A6:
<^o2,o3^> c= <^p2,p3^>
by Th32;
g in <^o2,o3^>
by A4;
then reconsider gg =
g as
Morphism of
p2,
p3 by A6;
A7:
<^o1,o2^> c= <^p1,p2^>
by Th32;
f in <^o1,o2^>
by A3;
then reconsider ff =
f as
Morphism of
p1,
p2 by A7;
A8:
(
<^o1,o3^> <> {} &
g * f = gg * ff )
by A3, A4, Th33, ALTCAT_1:def 2;
A9:
<^o3,o4^> c= <^p3,p4^>
by Th32;
h in <^o3,o4^>
by A5;
then reconsider hh =
h as
Morphism of
p3,
p4 by A9;
A10:
<^p3,p4^> <> {}
by A5, Th32, XBOOLE_1:3;
A11:
(
<^p1,p2^> <> {} &
<^p2,p3^> <> {} )
by A3, A4, Th32, XBOOLE_1:3;
(
<^o2,o4^> <> {} &
h * g = hh * gg )
by A4, A5, Th33, ALTCAT_1:def 2;
hence (h * g) * f =
(hh * gg) * ff
by A3, Th33
.=
hh * (gg * ff)
by A11, A10, Def8
.=
h * (g * f)
by A5, A8, Th33
;
verum
end;
hence
D is associative
; verum