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)
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 ;
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 A1:
<^o1,o2^> <> {}
and A2:
<^o2,o3^> <> {}
and A3:
<^o3,o4^> <> {}
;
(h * g) * f = h * (g * f)
A4:
<^o2,o3^> c= <^p2,p3^>
by Th31;
g in <^o2,o3^>
by A2;
then reconsider gg =
g as
Morphism of
p2,
p3 by A4;
A5:
<^o1,o2^> c= <^p1,p2^>
by Th31;
f in <^o1,o2^>
by A1;
then reconsider ff =
f as
Morphism of
p1,
p2 by A5;
A6:
(
<^o1,o3^> <> {} &
g * f = gg * ff )
by A1, A2, Th32, ALTCAT_1:def 2;
A7:
<^o3,o4^> c= <^p3,p4^>
by Th31;
h in <^o3,o4^>
by A3;
then reconsider hh =
h as
Morphism of
p3,
p4 by A7;
A8:
<^p3,p4^> <> {}
by A3, Th31, XBOOLE_1:3;
A9:
(
<^p1,p2^> <> {} &
<^p2,p3^> <> {} )
by A1, A2, Th31, XBOOLE_1:3;
(
<^o2,o4^> <> {} &
h * g = hh * gg )
by A2, A3, Th32, ALTCAT_1:def 2;
hence (h * g) * f =
(hh * gg) * ff
by A1, Th32
.=
hh * (gg * ff)
by A9, A8, Def8
.=
h * (g * f)
by A3, A6, Th32
;
verum
end;
hence
D is associative
; verum