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; :: according to MSAFREE4:def 7,MSAFREE4:def 8 :: thesis: Free (S,X) is free_in_itself
let f be ManySortedFunction of FreeGen X, the Sorts of (Free (S,X)); :: according to MSAFREE4:def 9 :: 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 non-empty 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