let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for X being V2() GeneratorSet of A st not A is finite-yielding holds
not FreeMSA X is finite-yielding
let A be non-empty MSAlgebra of S; :: thesis: for X being V2() GeneratorSet of A st not A is finite-yielding holds
not FreeMSA X is finite-yielding
let X be V2() 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
not the Sorts of A is finite-yielding by A1, MSAFREE2:def 11;
then consider i being set such that
A3: i in the carrier of S and
A4: not the Sorts of A . i is finite by FINSET_1:def 4;
the Sorts of (FreeMSA X) is finite-yielding by A2, MSAFREE2:def 11;
then A5: the Sorts of (FreeMSA X) . i is finite by A3, FINSET_1:def 4;
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 Th22;
reconsider i = i as Element of S by A3;
reconsider Fi = F . i as Function of FXi,SAi ;
F is "onto" by A6, MSUALG_3:def 8;
then rng Fi = SAi by MSUALG_3:def 3;
hence contradiction by A4, A5; :: thesis: verum