hereby :: according to PROB_2:def 3,
MSAFREE1:def 2 :: thesis: MSAlg C is feasible
let x,
y be
set ;
:: thesis: ( x <> y implies not the Sorts of (MSAlg C) . x meets the Sorts of (MSAlg C) . y )assume A1:
(
x <> y & the
Sorts of
(MSAlg C) . x meets the
Sorts of
(MSAlg C) . y )
;
:: thesis: contradictionthen consider z being
set such that A2:
(
z in the
Sorts of
(MSAlg C) . x &
z in the
Sorts of
(MSAlg C) . y )
by XBOOLE_0:3;
( the
Sorts of
(MSAlg C) . x <> {} & the
Sorts of
(MSAlg C) . y <> {} &
dom the
Sorts of
(MSAlg C) = the
carrier of
(CatSign the carrier of C) )
by A2, PARTFUN1:def 4;
then reconsider x =
x,
y =
y as
SortSymbol of
(CatSign the carrier of C) by FUNCT_1:def 4;
consider a,
b being
Object of
C such that A3:
x = homsym a,
b
by Th24;
consider c,
d being
Object of
C such that A4:
y = homsym c,
d
by Th24;
A5:
(
z in Hom a,
b &
z in Hom c,
d )
by A2, A3, A4, Def15;
then reconsider z =
z as
Morphism of
C ;
(
dom z = a &
dom z = c &
cod z = b &
cod z = d )
by A5, CAT_1:18;
hence
contradiction
by A1, A3, A4;
:: thesis: verum
end;
let o be OperSymbol of (CatSign the carrier of C); :: according to MSUALG_6:def 1 :: thesis: ( 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
;
:: thesis: ( Args o,(MSAlg C) = {} or not Result o,(MSAlg C) = {} )then consider a,
b,
c being
Object of
C such that A7:
o = compsym a,
b,
c
by Th27;
A8:
(
Args o,
(MSAlg C) = product <*(Hom b,c),(Hom a,b)*> &
Result o,
(MSAlg C) = Hom a,
c )
by A7, Th37;
consider A being
Element of
Args o,
(MSAlg C);
assume
Args o,
(MSAlg C) <> {}
;
:: thesis: not Result o,(MSAlg C) = {} then
ex
g,
f being
set st
(
g in Hom b,
c &
f in Hom a,
b &
A = <*g,f*> )
by A8, FUNCT_6:2;
hence
not
Result o,
(MSAlg C) = {}
by A8, CAT_1:52;
:: thesis: verum end;