let A, I be non empty reflexive AltCatStr ; :: thesis: for B being non empty reflexive SubCatStr of A
for C being non empty SubCatStr of A
for D being non empty SubCatStr of B st C = D holds
for F being FunctorStr over A,I holds F | C = (F | B) | D
let B be non empty reflexive SubCatStr of A; :: thesis: for C being non empty SubCatStr of A
for D being non empty SubCatStr of B st C = D holds
for F being FunctorStr over A,I holds F | C = (F | B) | D
let C be non empty SubCatStr of A; :: thesis: for D being non empty SubCatStr of B st C = D holds
for F being FunctorStr over A,I holds F | C = (F | B) | D
let D be non empty SubCatStr of B; :: thesis: ( C = D implies for F being FunctorStr over A,I holds F | C = (F | B) | D )
assume A1: C = D ; :: thesis: for F being FunctorStr over A,I holds F | C = (F | B) | D
let F be FunctorStr over A,I; :: thesis: F | C = (F | B) | D
thus F | C = F * ((incl B) * (incl D)) by A1, Th4
.= (F | B) | D by FUNCTOR0:32 ; :: thesis: verum