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 Def1;
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:8;
then A c= FreeGen (X (\/) ( the carrier of S --> {0})) by PBOOLE:def 18;
hence Free (S,X) is free by A1, EQUATION:28; :: thesis: verum