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 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 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, PARTFUN1:def 2;
then A15: [:<^a1,a2^>,<^a1,a1^>:] c= [:(Funcs (a1,a2)),(Funcs (a1,a1)):] by A14, RELAT_1:60;
<^a1,a1^> <> {} by A12, Th12;
hence <^a1,a2^> c= Funcs (a1,a2) by A15, ZFMISC_1:114; :: 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 A12, Th10; :: thesis: verum