thus for C1, C2 being strict with_triple-like_morphisms Category st the carrier of C1 = Hom o & ( for a, b being Element of Hom o
for f being Element of the carrier' of C st S₁[a,b,f] holds
[[a,b],f] is Morphism of C1 ) & ( for m being Morphism of C1 ex a, b being Element of Hom o ex f being Element of the carrier' of C st
( m = [[a,b],f] & S₁[a,b,f] ) ) & ( for m1, m2 being Morphism of C1
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],H₁(f2,f1)] ) & the carrier of C2 = Hom o & ( for a, b being Element of Hom o
for f being Element of the carrier' of C st S₁[a,b,f] holds
[[a,b],f] is Morphism of C2 ) & ( for m being Morphism of C2 ex a, b being Element of Hom o ex f being Element of the carrier' of C st
( m = [[a,b],f] & S₁[a,b,f] ) ) & ( for m1, m2 being Morphism of C2
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],H₁(f2,f1)] ) holds
C1 = C2 from CAT_5:sch 2(A6); :: thesis: verum