set v = the ManySortedMSSet of the Sorts of (Free (S,X)), the Sorts of (Free (S,X));
set 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)) #);
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)) #) is X,S -terms

proof

thus the Sorts of 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)) #) c= the Sorts of (Free (S,X)) ; :: according to PBOOLE:def 18,MSAFREE4:def 6 :: thesis: verum

end;

then reconsider 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)) #) as X,S -terms strict VarMSAlgebra over S ;
take A ; :: thesis: ( A is all_vars_including & A is inheriting_operations & A is free_in_itself )
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; :: according to MSAFREE4:def 7,MSAFREE4:def 8 :: thesis: A is free_in_itself
reconsider B = A as non-empty VarMSAlgebra over S ;
let f be ManySortedFunction of FreeGen X, the Sorts of A; :: according to MSAFREE4:def 9 :: 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 non-empty GeneratorSet of MSAlgebra(# the Sorts of B, the Charact of B #) by MSAFREE3:31;
reconsider H = F as non-empty GeneratorSet of B 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