let S be non void Signature; :: thesis: for X being ManySortedSet of holds
( Free S,X is feasible & Free S,X is free )
let X be ManySortedSet of ; :: 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 & 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 A1, 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