let B be non empty transitive SubCatStr of A; :: thesis: B is semi-functional

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 b_{1} being Element of <^b1,b2^>

for b_{2} being Element of <^b2,b3^>

for b_{3}, b_{4} being set holds

( not b_{1} = b_{3} or not b_{2} = b_{4} or b_{2} * b_{1} = b_{3} * b_{4} ) )

assume that

A1: <^b1,b2^> <> {} and

A2: <^b2,b3^> <> {} and

A3: <^b1,b3^> <> {} ; :: thesis: for b_{1} being Element of <^b1,b2^>

for b_{2} being Element of <^b2,b3^>

for b_{3}, b_{4} being set holds

( not b_{1} = b_{3} or not b_{2} = b_{4} or b_{2} * b_{1} = b_{3} * b_{4} )

reconsider a1 = b1, a2 = b2, a3 = b3 as Object of A by ALTCAT_2:29;

A4: ( <^a1,a2^> <> {} & <^a2,a3^> <> {} ) by A1, A2, ALTCAT_2:31, XBOOLE_1:3;

let f1 be Morphism of b1,b2; :: thesis: for b_{1} being Element of <^b2,b3^>

for b_{2}, b_{3} being set holds

( not f1 = b_{2} or not b_{1} = b_{3} or b_{1} * f1 = b_{2} * b_{3} )

let f2 be Morphism of b2,b3; :: thesis: for b_{1}, b_{2} being set holds

( not f1 = b_{1} or not f2 = b_{2} or f2 * f1 = b_{1} * b_{2} )

reconsider g2 = f2 as Morphism of a2,a3 by A2, ALTCAT_2:33;

reconsider g1 = f1 as Morphism of a1,a2 by A1, ALTCAT_2:33;

A5: <^a1,a3^> <> {} by A3, ALTCAT_2:31, XBOOLE_1:3;

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 A4, A5, ALTCAT_1:def 12;

hence f2 * f1 = f9 * g9 by A1, A2, ALTCAT_2:32; :: thesis: verum

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 b

for b

for b

( not b

assume that

A1: <^b1,b2^> <> {} and

A2: <^b2,b3^> <> {} and

A3: <^b1,b3^> <> {} ; :: thesis: for b

for b

for b

( not b

reconsider a1 = b1, a2 = b2, a3 = b3 as Object of A by ALTCAT_2:29;

A4: ( <^a1,a2^> <> {} & <^a2,a3^> <> {} ) by A1, A2, ALTCAT_2:31, XBOOLE_1:3;

let f1 be Morphism of b1,b2; :: thesis: for b

for b

( not f1 = b

let f2 be Morphism of b2,b3; :: thesis: for b

( not f1 = b

reconsider g2 = f2 as Morphism of a2,a3 by A2, ALTCAT_2:33;

reconsider g1 = f1 as Morphism of a1,a2 by A1, ALTCAT_2:33;

A5: <^a1,a3^> <> {} by A3, ALTCAT_2:31, XBOOLE_1:3;

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 A4, A5, ALTCAT_1:def 12;

hence f2 * f1 = f9 * g9 by A1, A2, ALTCAT_2:32; :: thesis: verum