let S be non void Signature; :: thesis: for X being ManySortedSet of the carrier of S holds
( Free S,X is feasible & Free S,X is free )
let X be ManySortedSet of the carrier of S; :: thesis: ( Free S,X is feasible & Free S,X is free )
set Y = X \/ (the carrier of S --> {0 });
consider A being MSSubset of (FreeMSA (X \/ (the carrier of S --> {0 }))) such that
A1: Free S,X = GenMSAlg A and
A2: A = (Reverse (X \/ (the carrier of S --> {0 }))) "" X by Def2;
thus Free S,X is feasible by A1; :: thesis: Free S,X is free
A is ManySortedSubset of FreeGen (X \/ (the carrier of S --> {0 })) by A2, EQUATION:9;
then A c= FreeGen (X \/ (the carrier of S --> {0 })) by PBOOLE:def 23;
hence Free S,X is free by A1, EQUATION:30; :: thesis: verum