thus the Sorts of (Free (S,X)) is ManySortedSubset of the Sorts of (Free (S,X)) :: according to MSAFREE4:def 6 :: thesis: ( FreeGen X is ManySortedSubset of the Sorts of (Free (S,X)) & ( for o being OperSymbol of S
for p being FinSequence st p in Args (o,(Free (S,X))) & (Den (o,(Free (S,X)))) . p in the Sorts of (Free (S,X)) . (the_result_sort_of o) holds
( p in Args (o,(Free (S,X))) & (Den (o,(Free (S,X)))) . p = (Den (o,(Free (S,X)))) . p ) ) & ( for f being ManySortedFunction of FreeGen X, the Sorts of (Free (S,X))
for G being ManySortedSubset of the Sorts of (Free (S,X)) st G = FreeGen X holds
ex h being ManySortedFunction of (Free (S,X)),(Free (S,X)) st
( h is_homomorphism Free (S,X), Free (S,X) & f = h || G ) ) )

proof

thus the Sorts of (Free (S,X)) c= the Sorts of (Free (S,X)) ; :: according to PBOOLE:def 18 :: thesis: verum

end;

set A = Free (S,X);
A1: Free (S,X) = FreeMSA X by MSAFREE3:31;
thus ( FreeGen X is ManySortedSubset of the Sorts of (Free (S,X)) & ( for o being OperSymbol of S
for p being FinSequence st p in Args (o,(Free (S,X))) & (Den (o,(Free (S,X)))) . p in the Sorts of (Free (S,X)) . (the_result_sort_of o) holds
( p in Args (o,(Free (S,X))) & (Den (o,(Free (S,X)))) . p = (Den (o,(Free (S,X)))) . p ) ) ) by MSAFREE3:31; :: thesis: for f being ManySortedFunction of FreeGen X, the Sorts of (Free (S,X))
for G being ManySortedSubset of the Sorts of (Free (S,X)) st G = FreeGen X holds
ex h being ManySortedFunction of (Free (S,X)),(Free (S,X)) st
( h is_homomorphism Free (S,X), Free (S,X) & f = h || G )
let f be ManySortedFunction of FreeGen X, the Sorts of (Free (S,X)); :: thesis: for G being ManySortedSubset of the Sorts of (Free (S,X)) st G = FreeGen X holds
ex h being ManySortedFunction of (Free (S,X)),(Free (S,X)) st
( h is_homomorphism Free (S,X), Free (S,X) & f = h || G )
let G be MSSubset of (Free (S,X)); :: thesis: ( G = FreeGen X implies ex h being ManySortedFunction of (Free (S,X)),(Free (S,X)) st
( h is_homomorphism Free (S,X), Free (S,X) & f = h || G ) )
assume A2: G = FreeGen X ; :: thesis: ex h being ManySortedFunction of (Free (S,X)),(Free (S,X)) st
( h is_homomorphism Free (S,X), Free (S,X) & f = h || G )
then reconsider H = G as V5() GeneratorSet of Free (S,X) by MSAFREE3:31;
thus ex h being ManySortedFunction of (Free (S,X)),(Free (S,X)) st
( h is_homomorphism Free (S,X), Free (S,X) & f = h || G ) by A2, A1, MSAFREE:def 5; :: thesis: verum