let A, B be semi-functional para-functional category; :: thesis:
now :: thesis: for a1, a2, a3 being Object of A st <^a1,a2^> <> {} & <^a2,a3^> <> {} holds
for b1, b2, b3 being Object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds
for f1 being Morphism of a1,a2
for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1
let a1, a2, a3 be Object of A; :: thesis: ( <^a1,a2^> <> {} & <^a2,a3^> <> {} implies for b1, b2, b3 being Object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds
for f1 being Morphism of a1,a2
for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1 )

assume that
A1: <^a1,a2^> <> {} and
A2: <^a2,a3^> <> {} ; :: thesis: for b1, b2, b3 being Object of B st <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 holds
for f1 being Morphism of a1,a2
for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1

let b1, b2, b3 be Object of B; :: thesis: ( <^b1,b2^> <> {} & <^b2,b3^> <> {} & b1 = a1 & b2 = a2 & b3 = a3 implies for f1 being Morphism of a1,a2
for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1 )

assume that
A3: ( <^b1,b2^> <> {} & <^b2,b3^> <> {} ) and
b1 = a1 and
b2 = a2 and
b3 = a3 ; :: thesis: for f1 being Morphism of a1,a2
for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1

let f1 be Morphism of a1,a2; :: thesis: for g1 being Morphism of b1,b2 st g1 = f1 holds
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1

let g1 be Morphism of b1,b2; :: thesis: ( g1 = f1 implies for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1 )

assume A4: g1 = f1 ; :: thesis: for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1

reconsider f = f1 as Function of (),() by ;
let f2 be Morphism of a2,a3; :: thesis: for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1

let g2 be Morphism of b2,b3; :: thesis: ( g2 = f2 implies f2 * f1 = g2 * g1 )
assume A5: g2 = f2 ; :: thesis: f2 * f1 = g2 * g1
A6: <^b1,b3^> <> {} by ;
reconsider g = f2 as Function of (),() by ;
<^a1,a3^> <> {} by ;
hence f2 * f1 = g * f by
.= g2 * g1 by ;
:: thesis: verum
end;
hence A,B have_the_same_composition by Th11; :: thesis: verum