hereby PROB_2:def 3,
MSAFREE1:def 2 MSAlg C is feasible
let x,
y be
set ;
( 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
set 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 4;
then reconsider x =
x,
y =
y as
SortSymbol of
(CatSign the carrier of C) by A3, A4, FUNCT_1:def 4;
consider a,
b being
Object of
C such that A5:
x = homsym a,
b
by Th24;
A6:
z in Hom a,
b
by A3, A5, Def15;
consider c,
d being
Object of
C such that A7:
y = homsym c,
d
by Th24;
A8:
z in Hom c,
d
by A4, A7, Def15;
reconsider z =
z as
Morphism of
C by A6;
A9:
(
dom z = a &
cod z = b )
by A6, CAT_1:18;
dom z = c
by A8, CAT_1:18;
hence
contradiction
by A1, A5, A7, A8, A9, CAT_1:18;
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 Th25;
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 Th27;
consider A being
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, Th37;
then A13:
ex
g,
f being
set st
(
g in Hom b,
c &
f in Hom a,
b &
A = <*g,f*> )
by A12, FUNCT_6:2;
Result o,
(MSAlg C) = Hom a,
c
by A11, Th37;
hence
not
Result o,
(MSAlg C) = {}
by A13, CAT_1:52;
verum end;