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
consider Av being non empty set such that
A2: ( Av = the Sorts of A . v & 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;
set Ov = { o where o is OperSymbol of S : the_result_sort_of o = v } ;
A3: { o where o is OperSymbol of S : the_result_sort_of o = v } is finite by A1, Def6;

A4: now

assume A5: { 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
A6: c in Constants A,v by XBOOLE_0:def 1;
consider a being Element of Av such that
A7: ( a = c & 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, A6;
consider o being OperSymbol of S such that
A8: ( the Arity of S . o = {} & the ResultSort of S . o = v & 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 { o where o is OperSymbol of S : the_result_sort_of o = v } by A8;
hence contradiction by A5; :: thesis: verum

end;

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

end;

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 ;
defpred S₁[ Element of Ov] means the Arity of S . $1 = {} ;
set COv = { o where o is Element of Ov : S₁[o] } ;
{ o where o is Element of Ov : S₁[o] } is Subset of Ov from DOMAIN_1:sch 7();
then A9: { o where o is Element of Ov : S₁[o] } is finite by A3;
deffunc H₁( Element of the carrier' of S) -> set = (Den $1,A) . {} ;
set aCOv = { H₁(o) where o is Element of the carrier' of S : o in { o where o is Element of Ov : S₁[o] } } ;
A10: { 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(A9);
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
A11: ( a = c & 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
A12: ( the Arity of S . o = {} & the ResultSort of S . o = v & a in rng (Den o,A) ) by A11;
the_result_sort_of o = the ResultSort of S . o by MSUALG_1:def 7;
then o in Ov by A12;
then reconsider o' = o as Element of Ov ;
A13: o' in { o where o is Element of Ov : S₁[o] } by A12;
set f = Den o,A;
A14: dom (Den o,A) = {{} } by A12, Th25;
consider x being set such that
A15: ( x in dom (Den o,A) & a = (Den o,A) . x ) by A12, FUNCT_1:def 5;
x = {} by A14, A15, 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 A11, A13, A15; :: thesis: verum

end;

hence Constants A,v is finite by A10; :: thesis: verum

end;

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