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:
not D is empty
by A1;
A4:
D is transitive
proof
let o1,
o2,
o3 be
object of
D;
:: according to ALTCAT_1:def 4 :: thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )
reconsider p1 =
o1,
p2 =
o2,
p3 =
o3 as
object of
C by A1;
A5:
<^o1,o2^> = <^p1,p2^>
by A2;
A6:
<^o2,o3^> = <^p2,p3^>
by A2;
A7:
<^o1,o3^> = <^p1,p3^>
by A2;
assume
(
<^o1,o2^> <> {} &
<^o2,o3^> <> {} )
;
:: thesis: not <^o1,o3^> = {}
hence
not
<^o1,o3^> = {}
by A5, A6, A7, ALTCAT_1:def 4;
:: thesis: verum
end;
C is SubCatStr of C
by Th21;
then
C is SubCatStr of D
by A1, A2, A3, A4, Th25;
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 Th23; :: thesis: verum