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

.= <^p1,p2^> by Def13 ;

:: thesis: verum

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

.= <^p1,p2^> by Def13 ;

:: thesis: verum