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

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