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 A13:
( 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 A14:
<^a1,a2^> <> {}
;
:: thesis: <^a1,a2^> c= Funcs a1,a2
<^a1,a1^> <> {}
by A13, Th21;
then A15:
[:<^a1,a2^>,<^a1,a1^>:] <> {}
by A14;
set c = the
Comp of
C . a1,
a1,
a2;
set f =
FuncComp (Funcs a1,a1),
(Funcs a1,a2);
A16:
dom (the Comp of C . a1,a1,a2) = [:<^a1,a2^>,<^a1,a1^>:]
by A14, FUNCT_2:def 1;
A17:
dom (FuncComp (Funcs a1,a1),(Funcs a1,a2)) = [:(Funcs a1,a2),(Funcs a1,a1):]
by PARTFUN1:def 4;
the
Comp of
C . a1,
a1,
a2 = (FuncComp (Funcs a1,a1),(Funcs a1,a2)) | [:<^a1,a2^>,<^a1,a1^>:]
by A13, Def15;
then
[:<^a1,a2^>,<^a1,a1^>:] c= [:(Funcs a1,a2),(Funcs a1,a1):]
by A16, A17, RELAT_1:89;
hence
<^a1,a2^> c= Funcs a1,
a2
by A15, ZFMISC_1:138;
:: thesis: verum 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 f', g' being Function st f = f' & g = g' holds
g * f = g' * f' )
thus
( <^a1,a2^> <> {} & <^a2,a3^> <> {} & <^a1,a3^> <> {} implies for f being Morphism of a1,a2
for g being Morphism of a2,a3
for f', g' being Function st f = f' & g = g' holds
g * f = g' * f' )
by A13, Th18; :: thesis: verum