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

hence
A,B have_the_same_composition
by Th11; :: thesis: verumfor 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;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