let A, B be semi-functional para-functional category; :: thesis: A,B have_the_same_composition

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 (the_carrier_of a1),(the_carrier_of a2) by A1, YELLOW18:34;
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 A3, ALTCAT_1:def 2;
reconsider g = f2 as Function of (the_carrier_of a2),(the_carrier_of a3) by A2, YELLOW18:34;
<^a1,a3^> <> {} by A1, A2, ALTCAT_1:def 2;
hence f2 * f1 = g * f by A1, A2, ALTCAT_1:def 12
.= g2 * g1 by A3, A4, A5, A6, ALTCAT_1:def 12 ;
:: thesis: verum

end;

hence A,B have_the_same_composition by Th11; :: thesis: verum