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

( 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