let B be non empty transitive SubCatStr of A; :: thesis:
let b1, b2, b3 be Object of B; :: according to ALTCAT_1:def 12 :: thesis: ( <^b1,b2^> = {} or <^b2,b3^> = {} or <^b1,b3^> = {} or for b1 being Element of <^b1,b2^>
for b2 being Element of <^b2,b3^>
for b3, b4 being set holds
( not b1 = b3 or not b2 = b4 or b2 * b1 = b3 * b4 ) )

assume that
A1: <^b1,b2^> <> {} and
A2: <^b2,b3^> <> {} and
A3: <^b1,b3^> <> {} ; :: thesis: for b1 being Element of <^b1,b2^>
for b2 being Element of <^b2,b3^>
for b3, b4 being set holds
( not b1 = b3 or not b2 = b4 or b2 * b1 = b3 * b4 )

reconsider a1 = b1, a2 = b2, a3 = b3 as Object of A by ALTCAT_2:29;
A4: ( <^a1,a2^> <> {} & <^a2,a3^> <> {} ) by ;
let f1 be Morphism of b1,b2; :: thesis: for b1 being Element of <^b2,b3^>
for b2, b3 being set holds
( not f1 = b2 or not b1 = b3 or b1 * f1 = b2 * b3 )

let f2 be Morphism of b2,b3; :: thesis: for b1, b2 being set holds
( not f1 = b1 or not f2 = b2 or f2 * f1 = b1 * b2 )

reconsider g2 = f2 as Morphism of a2,a3 by ;
reconsider g1 = f1 as Morphism of a1,a2 by ;
A5: <^a1,a3^> <> {} by ;
let f9, g9 be Function; :: thesis: ( not f1 = f9 or not f2 = g9 or f2 * f1 = f9 * g9 )
assume ( f1 = f9 & f2 = g9 ) ; :: thesis: f2 * f1 = f9 * g9
then g2 * g1 = g9 * f9 by ;
hence f2 * f1 = f9 * g9 by ; :: thesis: verum