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

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

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, 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
let a1, a2 be Object of C; :: according to ALTCAT_1:def 11 :: thesis: <^a1,a2^> c= Funcs (a1,a2)

end;per cases
( <^a1,a2^> = {} or <^a1,a2^> <> {} )
;

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;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

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