let A, B be semi-functional para-functional category; A,B have_the_same_composition
now 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 * g1let a1,
a2,
a3 be
Object of
A;
( <^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^> <> {}
;
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 * g1let b1,
b2,
b3 be
Object of
B;
( <^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
;
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 * g1let f1 be
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 * g1let g1 be
Morphism of
b1,
b2;
( 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
;
for f2 being Morphism of a2,a3
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1reconsider f =
f1 as
Function of
(the_carrier_of a1),
(the_carrier_of a2) by A1, YELLOW18:34;
let f2 be
Morphism of
a2,
a3;
for g2 being Morphism of b2,b3 st g2 = f2 holds
f2 * f1 = g2 * g1let g2 be
Morphism of
b2,
b3;
( g2 = f2 implies f2 * f1 = g2 * g1 )assume A5:
g2 = f2
;
f2 * f1 = g2 * g1A6:
<^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
;
verum end;
hence
A,B have_the_same_composition
by Th11; verum