let B be non empty transitive SubCatStr of A; :: thesis: B is semi-functional
let b1, b2, b3 be object of ; :: according to ALTCAT_1:def 14 :: 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 by ALTCAT_2:30;
A4: ( <^a1,a2^> <> {} & <^a2,a3^> <> {} ) by A1, A2, ALTCAT_2:32, XBOOLE_1:3;
let f1 be Morphism of ,; :: 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 ,; :: 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 , by A2, ALTCAT_2:34;
reconsider g1 = f1 as Morphism of , by A1, ALTCAT_2:34;
A5: <^a1,a3^> <> {} by A3, ALTCAT_2:32, XBOOLE_1:3;
let f', g' be Function; :: thesis: ( not f1 = f' or not f2 = g' or f2 * f1 = f' * g' )
assume ( f1 = f' & f2 = g' ) ; :: thesis: f2 * f1 = f' * g'
then g2 * g1 = g' * f' by A4, A5, ALTCAT_1:def 14;
hence f2 * f1 = f' * g' by A1, A2, ALTCAT_2:33; :: thesis: verum