let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for v being SortSymbol of S st S is finitely_operated holds
Constants (A,v) is finite
let A be non-empty MSAlgebra over S; :: thesis: for v being SortSymbol of S st S is finitely_operated holds
Constants (A,v) is finite
let v be SortSymbol of S; :: thesis: ( S is finitely_operated implies Constants (A,v) is finite )
assume A1: S is finitely_operated ; :: thesis: Constants (A,v) is finite
set Ov = { o where o is OperSymbol of S : the_result_sort_of o = v } ;
consider Av being non empty set such that
Av = the Sorts of A . v and
A2: Constants (A,v) = { a where a is Element of Av : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = v & a in rng (Den (o,A)) ) } by MSUALG_2:def 3;
A3: { o where o is OperSymbol of S : the_result_sort_of o = v } is finite by A1;

A4: now :: thesis: ( not { o where o is OperSymbol of S : the_result_sort_of o = v } is empty implies Constants (A,v) is finite )

assume not { o where o is OperSymbol of S : the_result_sort_of o = v } is empty ; :: thesis: Constants (A,v) is finite
then reconsider Ov = { o where o is OperSymbol of S : the_result_sort_of o = v } as non empty set ;
deffunc H₁( Element of the carrier' of S) -> set = (Den ($1,A)) . {};
defpred S₁[ Element of Ov] means the Arity of S . $1 = {} ;
set COv = { o where o is Element of Ov : S₁[o] } ;
set aCOv = { H₁(o) where o is Element of the carrier' of S : o in { o where o is Element of Ov : S₁[o] } } ;
A5: Constants (A,v) c= { H₁(o) where o is Element of the carrier' of S : o in { o where o is Element of Ov : S₁[o] } }

proof

let c be object ; :: according to TARSKI:def 3 :: thesis: ( not c in Constants (A,v) or c in { H₁(o) where o is Element of the carrier' of S : o in { o where o is Element of Ov : S₁[o] } } )
assume c in Constants (A,v) ; :: thesis: c in { H₁(o) where o is Element of the carrier' of S : o in { o where o is Element of Ov : S₁[o] } }
then consider a being Element of Av such that
A6: a = c and
A7: ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = v & a in rng (Den (o,A)) ) by A2;
consider o being OperSymbol of S such that
A8: the Arity of S . o = {} and
A9: the ResultSort of S . o = v and
A10: a in rng (Den (o,A)) by A7;
the_result_sort_of o = the ResultSort of S . o by MSUALG_1:def 2;
then o in Ov by A9;
then reconsider o9 = o as Element of Ov ;
A11: o9 in { o where o is Element of Ov : S₁[o] } by A8;
set f = Den (o,A);
consider x being object such that
A12: x in dom (Den (o,A)) and
A13: a = (Den (o,A)) . x by A10, FUNCT_1:def 3;
dom (Den (o,A)) = {{}} by A8, Th23;
then x = {} by A12, TARSKI:def 1;
hence c in { H₁(o) where o is Element of the carrier' of S : o in { o where o is Element of Ov : S₁[o] } } by A6, A11, A13; :: thesis: verum

end;

{ o where o is Element of Ov : S₁[o] } is Subset of Ov from DOMAIN_1:sch 7();
then A14: { o where o is Element of Ov : S₁[o] } is finite by A3;
{ H₁(o) where o is Element of the carrier' of S : o in { o where o is Element of Ov : S₁[o] } } is finite from FRAENKEL:sch 21(A14);
hence Constants (A,v) is finite by A5; :: thesis: verum

end;

now :: thesis: ( { o where o is OperSymbol of S : the_result_sort_of o = v } is empty implies Constants (A,v) is finite )

assume A15: { o where o is OperSymbol of S : the_result_sort_of o = v } is empty ; :: thesis: Constants (A,v) is finite

now :: thesis: Constants (A,v) is empty

assume not Constants (A,v) is empty ; :: thesis: contradiction
then consider c being object such that
A16: c in Constants (A,v) by XBOOLE_0:def 1;
consider a being Element of Av such that
a = c and
A17: ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = v & a in rng (Den (o,A)) ) by A2, A16;
consider o being OperSymbol of S such that
the Arity of S . o = {} and
A18: the ResultSort of S . o = v and
a in rng (Den (o,A)) by A17;
the_result_sort_of o = the ResultSort of S . o by MSUALG_1:def 2;
then o in { o where o is OperSymbol of S : the_result_sort_of o = v } by A18;
hence contradiction by A15; :: thesis: verum

end;

hence Constants (A,v) is finite ; :: thesis: verum

end;

hence Constants (A,v) is finite by A4; :: thesis: verum