let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for v being SortSymbol of S st S is finitely_operated holds
Constants A,v is finite
let A be non-empty MSAlgebra of 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 4;
A3: { o where o is OperSymbol of S : the_result_sort_of o = v } is finite by A1, Def6;

A4: now

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 set ; :: 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 7;
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 set such that
A12: x in dom (Den o,A) and
A13: a = (Den o,A) . x by A10, FUNCT_1:def 5;
dom (Den o,A) = {{} } by A8, Th25;
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

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

now

assume not Constants A,v is empty ; :: thesis: contradiction
then consider c being set 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 7;
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