let C be non empty AltCatStr ; :: thesis: for D being non empty full SubCatStr of C
for o1, o2 being object of C
for p1, p2 being object of D st o1 = p1 & o2 = p2 holds
<^o1,o2^> = <^p1,p2^>
let D be non empty full SubCatStr of C; :: thesis: for o1, o2 being object of C
for p1, p2 being object of D st o1 = p1 & o2 = p2 holds
<^o1,o2^> = <^p1,p2^>
let o1, o2 be object of C; :: thesis: for p1, p2 being object of D st o1 = p1 & o2 = p2 holds
<^o1,o2^> = <^p1,p2^>
let p1, p2 be object of D; :: thesis: ( o1 = p1 & o2 = p2 implies <^o1,o2^> = <^p1,p2^> )
assume A1: ( o1 = p1 & o2 = p2 ) ; :: thesis: <^o1,o2^> = <^p1,p2^>
[p1,p2] in [:the carrier of D,the carrier of D:] ;
hence <^o1,o2^> = (the Arrows of C || the carrier of D) . p1,p2 by A1, FUNCT_1:72
.= <^p1,p2^> by Def13 ;
:: thesis: verum