let S be non empty non void ManySortedSign ; :: thesis: ( S is finitely_operated & InducedGraph S is well-founded implies S is monotonic )
set G = InducedGraph S;
assume that
A1: S is finitely_operated and
A2: InducedGraph S is well-founded ; :: thesis: S is monotonic
given A being non-empty finitely-generated MSAlgebra over S such that A3: not A is finite-yielding ; :: according to MSAFREE2:def 13 :: thesis: contradiction
set GS = the V2() V39() GeneratorSet of A;
reconsider gs = the V2() V39() GeneratorSet of A as V2() V39() ManySortedSet of the carrier of S ;
not FreeMSA gs is finite-yielding by A3, MSSCYC_1:23;
then the Sorts of (FreeMSA gs) is V39() ;
then consider v being object such that
A4: v in the carrier of S and
A5: not the Sorts of (FreeMSA gs) . v is finite by FINSET_1:def 5;
reconsider v = v as SortSymbol of S by A4;
consider n being Nat such that
A6: for c being directed Chain of InducedGraph S st not c is empty & (vertex-seq c) . ((len c) + 1) = v holds
len c <= n by A2, MSSCYC_1:def 4;
set V = the Sorts of (FreeMSA gs) . v;
set Vn = { t where t is Element of the Sorts of (FreeMSA gs) . v : depth t <= n } ;
{ t where t is Element of the Sorts of (FreeMSA gs) . v : depth t <= n } is finite by A1, Th5;
then not the Sorts of (FreeMSA gs) . v c= { t where t is Element of the Sorts of (FreeMSA gs) . v : depth t <= n } by A5;
then consider t being object such that
A7: t in the Sorts of (FreeMSA gs) . v and
A8: not t in { t where t is Element of the Sorts of (FreeMSA gs) . v : depth t <= n } ;
reconsider t = t as Element of the Sorts of (FreeMSA gs) . v by A7;
A9: not depth t <= n by A8;
then 1 <= depth t by NAT_1:14;
then ex d being directed Chain of InducedGraph S st
( len d = depth t & (vertex-seq d) . ((len d) + 1) = v ) by Th2;
hence contradiction by A6, A9, CARD_1:27; :: thesis: verum