let S be non empty non void ManySortedSign ; :: thesis:
let U0 be free feasible MSAlgebra over S; :: thesis:
let A be free GeneratorSet of U0; :: thesis:
let Z be MSSubset of U0; :: thesis:
assume that
A1: Z c= A and
A2: GenMSAlg Z is feasible ; :: thesis:
reconsider Z1 = Z as MSSubset of (GenMSAlg Z) by MSUALG_2:def 17;
the Sorts of (GenMSAlg Z1) = the Sorts of (GenMSAlg Z) by EXTENS_1:18;
then reconsider z = Z as GeneratorSet of GenMSAlg Z by MSAFREE:def 4;
reconsider z1 = z as ManySortedSubset of A by A1, PBOOLE:def 18;
take z ; :: according to MSAFREE:def 6 :: thesis:
z is free

proof

reconsider D = the Sorts of (GenMSAlg Z) as MSSubset of U0 by MSUALG_2:def 9;
let U1 be non-empty MSAlgebra over S; :: according to MSAFREE:def 5 :: thesis:
let g be ManySortedFunction of z, the Sorts of U1; :: thesis:
consider G being ManySortedFunction of A, the Sorts of U1 such that
A3: G || z1 = g by Th6;
consider h being ManySortedFunction of U0,U1 such that
A4: h is_homomorphism U0,U1 and
A5: h || A = G by MSAFREE:def 5;
reconsider H = h || D as ManySortedFunction of (GenMSAlg Z),U1 ;
take H ; :: thesis:
thus H is_homomorphism GenMSAlg Z,U1 by A2, A4, Th22; :: thesis:
thus g = h || Z by A3, A5, Th5
.= H || z by Th5 ; :: thesis:

end;

hence z is free ; :: thesis: