let C be non empty AltCatStr ; ( 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 )
; ( C is quasi-functional & C is semi-functional )
thus
C is quasi-functional
C is semi-functional proof
let a1,
a2 be
Object of
C;
ALTCAT_1:def 11 <^a1,a2^> c= Funcs (a1,a2)
per cases
( <^a1,a2^> = {} or <^a1,a2^> <> {} )
;
suppose A13:
<^a1,a2^> <> {}
;
<^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;
verum end;
end;
let a1, a2, a3 be Object of C; ALTCAT_1:def 12 ( <^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; verum