let S be non empty void ManySortedSign ; :: thesis: ( S is monotonic iff InducedGraph S is well-founded )

set G = InducedGraph S;

set OS = the carrier' of S;

set CA = the carrier of S;

set AR = the Arity of S;

let A be non-empty finitely-generated MSAlgebra over S; :: according to MSAFREE2:def 13 :: thesis: A is finite-yielding

thus the Sorts of A is V39() by MSAFREE2:def 10; :: according to MSAFREE2:def 11 :: thesis: verum

set G = InducedGraph S;

set OS = the carrier' of S;

set CA = the carrier of S;

set AR = the Arity of S;

hereby :: thesis: ( InducedGraph S is well-founded implies S is monotonic )

assume
InducedGraph S is well-founded
; :: thesis: S is monotonic assume
S is monotonic
; :: thesis: InducedGraph S is well-founded

assume not InducedGraph S is well-founded ; :: thesis: contradiction

then consider v being Element of the carrier of (InducedGraph S) such that

A1: for n being Nat ex c being directed Chain of InducedGraph S st

( not c is empty & (vertex-seq c) . ((len c) + 1) = v & len c > n ) by MSSCYC_1:def 4;

consider e being directed Chain of InducedGraph S such that

A2: not e is empty and

(vertex-seq e) . ((len e) + 1) = v and

len e > 0 by A1;

e is FinSequence of the carrier' of (InducedGraph S) by MSSCYC_1:def 1;

then A3: rng e c= the carrier' of (InducedGraph S) by FINSEQ_1:def 4;

1 in dom e by A2, FINSEQ_5:6;

then e . 1 in rng e by FUNCT_1:def 3;

then ex op, v being set st

( e . 1 = [op,v] & op in the carrier' of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st

( the Arity of S . op = args & n in dom args & args . n = v ) ) by A3, Def1;

hence contradiction ; :: thesis: verum

end;assume not InducedGraph S is well-founded ; :: thesis: contradiction

then consider v being Element of the carrier of (InducedGraph S) such that

A1: for n being Nat ex c being directed Chain of InducedGraph S st

( not c is empty & (vertex-seq c) . ((len c) + 1) = v & len c > n ) by MSSCYC_1:def 4;

consider e being directed Chain of InducedGraph S such that

A2: not e is empty and

(vertex-seq e) . ((len e) + 1) = v and

len e > 0 by A1;

e is FinSequence of the carrier' of (InducedGraph S) by MSSCYC_1:def 1;

then A3: rng e c= the carrier' of (InducedGraph S) by FINSEQ_1:def 4;

1 in dom e by A2, FINSEQ_5:6;

then e . 1 in rng e by FUNCT_1:def 3;

then ex op, v being set st

( e . 1 = [op,v] & op in the carrier' of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st

( the Arity of S . op = args & n in dom args & args . n = v ) ) by A3, Def1;

hence contradiction ; :: thesis: verum

let A be non-empty finitely-generated MSAlgebra over S; :: according to MSAFREE2:def 13 :: thesis: A is finite-yielding

thus the Sorts of A is V39() by MSAFREE2:def 10; :: according to MSAFREE2:def 11 :: thesis: verum