let C be non empty transitive AltCatStr ; :: thesis: for D being SubCatStr of C st the carrier of D = the carrier of C & the Arrows of D = the Arrows of C holds

AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #)

let D be SubCatStr of C; :: thesis: ( the carrier of D = the carrier of C & the Arrows of D = the Arrows of C implies AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) )

assume that

A1: the carrier of D = the carrier of C and

A2: the Arrows of D = the Arrows of C ; :: thesis: AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #)

A3: D is transitive

not D is empty by A1;

then C is SubCatStr of D by A1, A2, A3, A6, Th24;

hence AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) by Th22; :: thesis: verum

AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #)

let D be SubCatStr of C; :: thesis: ( the carrier of D = the carrier of C & the Arrows of D = the Arrows of C implies AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) )

assume that

A1: the carrier of D = the carrier of C and

A2: the Arrows of D = the Arrows of C ; :: thesis: AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #)

A3: D is transitive

proof

A6:
C is SubCatStr of C
by Th20;
let o1, o2, o3 be Object of D; :: according to ALTCAT_1:def 2 :: thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )

reconsider p1 = o1, p2 = o2, p3 = o3 as Object of C by A1;

assume A4: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; :: thesis: not <^o1,o3^> = {}

A5: <^o1,o3^> = <^p1,p3^> by A2;

( <^o1,o2^> = <^p1,p2^> & <^o2,o3^> = <^p2,p3^> ) by A2;

hence not <^o1,o3^> = {} by A5, A4, ALTCAT_1:def 2; :: thesis: verum

end;reconsider p1 = o1, p2 = o2, p3 = o3 as Object of C by A1;

assume A4: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; :: thesis: not <^o1,o3^> = {}

A5: <^o1,o3^> = <^p1,p3^> by A2;

( <^o1,o2^> = <^p1,p2^> & <^o2,o3^> = <^p2,p3^> ) by A2;

hence not <^o1,o3^> = {} by A5, A4, ALTCAT_1:def 2; :: thesis: verum

not D is empty by A1;

then C is SubCatStr of D by A1, A2, A3, A6, Th24;

hence AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) by Th22; :: thesis: verum