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: C is semi-functional

proof

let a1, a2 be object of C; :: according to ALTCAT_1:def 13 :: 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 by XBOOLE_1:2; :: 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 A13, FUNCT_2:def 1;
( 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 A12, Def15, PARTFUN1:def 4;
then A15: [:<^a1,a2^>,<^a1,a1^>:] c= [:(Funcs a1,a2),(Funcs a1,a1):] by A14, RELAT_1:89;
<^a1,a1^> <> {} by A12, Th21;
hence <^a1,a2^> c= Funcs a1,a2 by A13, A15, ZFMISC_1:138; :: thesis: verum

end;

end;

end;

let a1, a2, a3 be object of C; :: according to ALTCAT_1:def 14 :: 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 A12, Th18; :: thesis: verum