set v = the ManySortedMSSet of the Sorts of (Free (S,X)), the Sorts of (Free (S,X));
take A = VarMSAlgebra(# the Sorts of (Free (S,X)), the Charact of (Free (S,X)), the ManySortedMSSet of the Sorts of (Free (S,X)), the Sorts of (Free (S,X)) #); :: thesis: A is X,S -terms
thus the Sorts of A is ManySortedSubset of the Sorts of (Free (S,X)) :: according to MSAFREE4:def 6 :: thesis: ( FreeGen X is ManySortedSubset of the Sorts of A & ( for b₁ being Element of the carrier' of S
for b₂ being set holds
( not b₂ in Args (b₁,(Free (S,X))) or not (Den (b₁,(Free (S,X)))) . b₂ in the Sorts of A . (the_result_sort_of b₁) or ( b₂ in Args (b₁,A) & (Den (b₁,A)) . b₂ = (Den (b₁,(Free (S,X)))) . b₂ ) ) ) & ( for b₁ being ManySortedFunction of FreeGen X, the Sorts of A
for b₂ being ManySortedSubset of the Sorts of A holds
( not b₂ = FreeGen X or ex b₃ being ManySortedFunction of the Sorts of A, the Sorts of A st
( b₃ is_homomorphism A,A & b₁ = b₃ || b₂ ) ) ) )

proof

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

end;

A1: MSAlgebra(# the Sorts of A, the Charact of A #) = FreeMSA X by MSAFREE3:31;
thus ( FreeGen X is ManySortedSubset of the Sorts of A & ( 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 A . (the_result_sort_of o) holds
( p in Args (o,A) & (Den (o,A)) . p = (Den (o,(Free (S,X)))) . p ) ) ) by MSAFREE3:31; :: thesis: for b₁ being ManySortedFunction of FreeGen X, the Sorts of A
for b₂ being ManySortedSubset of the Sorts of A holds
( not b₂ = FreeGen X or ex b₃ being ManySortedFunction of the Sorts of A, the Sorts of A st
( b₃ is_homomorphism A,A & b₁ = b₃ || b₂ ) )
let f be ManySortedFunction of FreeGen X, the Sorts of A; :: thesis: for b₁ being ManySortedSubset of the Sorts of A holds
( not b₁ = FreeGen X or ex b₂ being ManySortedFunction of the Sorts of A, the Sorts of A st
( b₂ is_homomorphism A,A & f = b₂ || b₁ ) )
let G be MSSubset of A; :: thesis: ( not G = FreeGen X or ex b₁ being ManySortedFunction of the Sorts of A, the Sorts of A st
( b₁ is_homomorphism A,A & f = b₁ || G ) )
assume A2: G = FreeGen X ; :: thesis: ex b₁ being ManySortedFunction of the Sorts of A, the Sorts of A st
( b₁ is_homomorphism A,A & f = b₁ || G )
then reconsider F = G as V2() GeneratorSet of MSAlgebra(# the Sorts of A, the Charact of A #) by MSAFREE3:31;
reconsider H = F as V2() GeneratorSet of A by Th32;
H is free by Th33, A1, A2, MSAFREE:16;
hence ex b₁ being ManySortedFunction of the Sorts of A, the Sorts of A st
( b₁ is_homomorphism A,A & f = b₁ || G ) by A2; :: thesis: verum