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

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