let D be non empty SubCatStr of C; :: thesis: ( D is transitive implies D is associative )
assume
D is transitive
; :: thesis: 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;
:: according to ALTCAT_2:def 8 :: thesis: 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 &
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;
let f be
Morphism of
o1,
o2;
:: thesis: 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;
:: thesis: 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;
:: thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} implies (h * g) * f = h * (g * f) )
assume that A2:
<^o1,o2^> <> {}
and A3:
<^o2,o3^> <> {}
and A4:
<^o3,o4^> <> {}
;
:: thesis: (h * g) * f = h * (g * f)
A5:
<^o1,o2^> c= <^p1,p2^>
by Th32;
A6:
<^p1,p2^> <> {}
by A2, Th32, XBOOLE_1:3;
A7:
<^o2,o3^> c= <^p2,p3^>
by Th32;
A8:
<^p2,p3^> <> {}
by A3, Th32, XBOOLE_1:3;
A9:
<^o3,o4^> c= <^p3,p4^>
by Th32;
A10:
<^p3,p4^> <> {}
by A4, Th32, XBOOLE_1:3;
A11:
<^o1,o3^> <> {}
by A2, A3, ALTCAT_1:def 4;
A12:
<^o2,o4^> <> {}
by A3, A4, ALTCAT_1:def 4;
f in <^o1,o2^>
by A2;
then reconsider ff =
f as
Morphism of
p1,
p2 by A5;
g in <^o2,o3^>
by A3;
then reconsider gg =
g as
Morphism of
p2,
p3 by A7;
h in <^o3,o4^>
by A4;
then reconsider hh =
h as
Morphism of
p3,
p4 by A9;
A13:
g * f = gg * ff
by A2, A3, Th33;
h * g = hh * gg
by A3, A4, Th33;
hence (h * g) * f =
(hh * gg) * ff
by A2, A12, Th33
.=
hh * (gg * ff)
by A6, A8, A10, Def8
.=
h * (g * f)
by A4, A11, A13, Th33
;
:: thesis: verum
end;
hence
D is associative
; :: thesis: verum