let C be non empty AltCatStr ; :: thesis: ( C is with_units & C is pseudo-functional & C is transitive implies ( C is quasi-functional & C is semi-functional ) )
assume A12: ( C is with_units & C is pseudo-functional & C is transitive ) ; :: thesis: ( C is quasi-functional & C is semi-functional )
thus C is quasi-functional :: thesis:
proof
let a1, a2 be Object of C; :: according to ALTCAT_1:def 11 :: thesis: <^a1,a2^> c= Funcs (a1,a2)
per cases ( <^a1,a2^> = {} or <^a1,a2^> <> {} ) ;
suppose <^a1,a2^> = {} ; :: thesis: <^a1,a2^> c= Funcs (a1,a2)
hence <^a1,a2^> c= Funcs (a1,a2) ; :: thesis: verum
end;
suppose A13: <^a1,a2^> <> {} ; :: thesis: <^a1,a2^> c= Funcs (a1,a2)
set c = the Comp of C . (a1,a1,a2);
set f = FuncComp ((Funcs (a1,a1)),(Funcs (a1,a2)));
A14: dom ( the Comp of C . (a1,a1,a2)) = [:<^a1,a2^>,<^a1,a1^>:] by ;
( dom (FuncComp ((Funcs (a1,a1)),(Funcs (a1,a2)))) = [:(Funcs (a1,a2)),(Funcs (a1,a1)):] & the Comp of C . (a1,a1,a2) = (FuncComp ((Funcs (a1,a1)),(Funcs (a1,a2)))) | [:<^a1,a2^>,<^a1,a1^>:] ) by ;
then A15: [:<^a1,a2^>,<^a1,a1^>:] c= [:(Funcs (a1,a2)),(Funcs (a1,a1)):] by ;
<^a1,a1^> <> {} by ;
hence <^a1,a2^> c= Funcs (a1,a2) by ; :: thesis: verum
end;
end;
end;
let a1, a2, a3 be Object of C; :: according to ALTCAT_1:def 12 :: thesis: ( <^a1,a2^> <> {} & <^a2,a3^> <> {} & <^a1,a3^> <> {} implies for f being Morphism of a1,a2
for g being Morphism of a2,a3
for f9, g9 being Function st f = f9 & g = g9 holds
g * f = g9 * f9 )

thus ( <^a1,a2^> <> {} & <^a2,a3^> <> {} & <^a1,a3^> <> {} implies for f being Morphism of a1,a2
for g being Morphism of a2,a3
for f9, g9 being Function st f = f9 & g = g9 holds
g * f = g9 * f9 ) by ; :: thesis: verum