let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for X being non-empty GeneratorSet of A st not A is finite-yielding holds
not FreeMSA X is finite-yielding
let A be non-empty MSAlgebra over S; :: thesis: for X being non-empty GeneratorSet of A st not A is finite-yielding holds
not FreeMSA X is finite-yielding
let X be non-empty GeneratorSet of A; :: thesis: ( not A is finite-yielding implies not FreeMSA X is finite-yielding )
assume that
A1: not A is finite-yielding and
A2: FreeMSA X is finite-yielding ; :: thesis: contradiction
the Sorts of A is finite-yielding by A1, MSAFREE2:def 11;
then consider i being object such that
A3: i in the carrier of S and
A4: the Sorts of A . i is infinite ;
the Sorts of (FreeMSA X) is finite-yielding by A2, MSAFREE2:def 11;
then A5: the Sorts of (FreeMSA X) . i is finite ;
reconsider FXi = the Sorts of (FreeMSA X) . i as non empty set by A3;
reconsider SAi = the Sorts of A . i as non empty set by A3;
consider F being ManySortedFunction of (FreeMSA X),A such that
A6: F is_epimorphism FreeMSA X,A by Th21;
reconsider i = i as Element of S by A3;
reconsider Fi = F . i as Function of FXi,SAi ;
F is "onto" by A6;
then rng Fi = SAi ;
hence contradiction by A4, A5; :: thesis: verum