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₁ being Element of <^b1,b2^>
for b₂ being Element of <^b2,b3^>
for b₃, b₄ being set holds
( not b₁ = b₃ or not b₂ = b₄ or b₂ * b₁ = b₃ * b₄ ) )
assume that
A1: <^b1,b2^> <> {} and
A2: <^b2,b3^> <> {} and
A3: <^b1,b3^> <> {} ; :: thesis: for b₁ being Element of <^b1,b2^>
for b₂ being Element of <^b2,b3^>
for b₃, b₄ being set holds
( not b₁ = b₃ or not b₂ = b₄ or b₂ * b₁ = b₃ * 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₁ being Element of <^b2,b3^>
for b₂, b₃ being set holds
( not f1 = b₂ or not b₁ = b₃ or b₁ * f1 = b₂ * b₃ )
let f2 be Morphism of b2,b3; :: thesis: for b₁, b₂ being set holds
( not f1 = b₁ or not f2 = b₂ or f2 * f1 = b₁ * 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