let C be non empty AltCatStr ; 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; 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; for p1, p2 being Object of D st o1 = p1 & o2 = p2 holds
<^o1,o2^> = <^p1,p2^>
let p1, p2 be Object of D; ( o1 = p1 & o2 = p2 implies <^o1,o2^> = <^p1,p2^> )
assume A1:
( o1 = p1 & o2 = p2 )
; <^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
;
verum