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

assume D is transitive ; :: thesis: D is associative

then reconsider D = D as non empty transitive SubCatStr of C ;

D is associative

proof

hence
D is associative
; :: thesis: verum
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)

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; :: 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

A1: <^o1,o2^> <> {} and

A2: <^o2,o3^> <> {} and

A3: <^o3,o4^> <> {} ; :: thesis: (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 ;

:: thesis: verum

end;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; :: 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

A1: <^o1,o2^> <> {} and

A2: <^o2,o3^> <> {} and

A3: <^o3,o4^> <> {} ; :: thesis: (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 ;

:: thesis: verum