A1: FreeMSA X = Free (S,X) by MSAFREE3:31;
reconsider H = FreeGen X as non-empty GeneratorSet of Free (S,X) by MSAFREE3:31;
H is MSSubset of A1 by Def7;
then reconsider f = id H as ManySortedFunction of H, the Sorts of A1 by Th22;
consider g being ManySortedFunction of (Free (S,X)),A1 such that
A2: ( g is_homomorphism Free (S,X),A1 & g || H = f ) by A1, MSAFREE:def 5;
take g ; :: thesis: ( g is_homomorphism Free (S,X),A1 & ( for G being GeneratorSet of Free (S,X) st G = FreeGen X holds
id G = g || G ) )
thus ( g is_homomorphism Free (S,X),A1 & ( for G being GeneratorSet of Free (S,X) st G = FreeGen X holds
id G = g || G ) ) by A2; :: thesis: verum