thus for C1, C2 being strict with_triple-like_morphisms Category st the carrier of C1 = o Hom & ( for a, b being Element of o Hom
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 o Hom 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 o Hom
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 = o Hom & ( for a, b being Element of o Hom
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 o Hom 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 o Hom
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(A21); :: thesis: verum