hereby PROB_2:def 2,
MSAFREE1:def 2 MSAlg C is feasible
let x,
y be
object ;
( x <> y implies not the Sorts of (MSAlg C) . x meets the Sorts of (MSAlg C) . y )assume that A1:
x <> y
and A2:
the
Sorts of
(MSAlg C) . x meets the
Sorts of
(MSAlg C) . y
;
contradictionconsider z being
object such that A3:
z in the
Sorts of
(MSAlg C) . x
and A4:
z in the
Sorts of
(MSAlg C) . y
by A2, XBOOLE_0:3;
dom the
Sorts of
(MSAlg C) = the
carrier of
(CatSign the carrier of C)
by PARTFUN1:def 2;
then reconsider x =
x,
y =
y as
SortSymbol of
(CatSign the carrier of C) by A3, A4, FUNCT_1:def 2;
consider a,
b being
Object of
C such that A5:
x = homsym (
a,
b)
by Th15;
A6:
z in Hom (
a,
b)
by A3, A5, Def13;
consider c,
d being
Object of
C such that A7:
y = homsym (
c,
d)
by Th15;
A8:
z in Hom (
c,
d)
by A4, A7, Def13;
reconsider z =
z as
Morphism of
C by A6;
A9:
(
dom z = a &
cod z = b )
by A6, CAT_1:1;
dom z = c
by A8, CAT_1:1;
hence
contradiction
by A1, A5, A7, A8, A9, CAT_1:1;
verum
end;
let o be OperSymbol of (CatSign the carrier of C); MSUALG_6:def 1 ( Args (o,(MSAlg C)) = {} or not Result (o,(MSAlg C)) = {} )
per cases
( o `1 = 1 or o `1 = 2 )
by Th16;
suppose
o `1 = 2
;
( Args (o,(MSAlg C)) = {} or not Result (o,(MSAlg C)) = {} )then consider a,
b,
c being
Object of
C such that A11:
o = compsym (
a,
b,
c)
by Th18;
set A = the
Element of
Args (
o,
(MSAlg C));
assume A12:
Args (
o,
(MSAlg C))
<> {}
;
not Result (o,(MSAlg C)) = {}
Args (
o,
(MSAlg C))
= product <*(Hom (b,c)),(Hom (a,b))*>
by A11, Th27;
then A13:
ex
g,
f being
object st
(
g in Hom (
b,
c) &
f in Hom (
a,
b) & the
Element of
Args (
o,
(MSAlg C))
= <*g,f*> )
by A12, FINSEQ_3:124;
Result (
o,
(MSAlg C))
= Hom (
a,
c)
by A11, Th27;
hence
not
Result (
o,
(MSAlg C))
= {}
by A13, CAT_1:24;
verum end;