thus
ex F being strict with_triple-like_morphisms Category st
( the carrier of F = Hom o & ( for a, b being Element of Hom o
for f being Element of the carrier' of C st S1[a,b,f] holds
[[a,b],f] is Morphism of F ) & ( for m being Morphism of F ex a, b being Element of Hom o ex f being Element of the carrier' of C st
( m = [[a,b],f] & S1[a,b,f] ) ) & ( for m1, m2 being Morphism of F
for a1, a2, a3 being Element of Hom o
for f1, f2 being Element of the carrier' of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2] holds
m2 (*) m1 = [[a1,a3],H1(f2,f1)] ) )
from CAT_5:sch 1(A1, A6, A9); verum