let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of S
for A, B being non-empty MSAlgebra over S st MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) & A is X,S -terms holds
B is X,S -terms
let X be V5() ManySortedSet of S; :: thesis: for A, B being non-empty MSAlgebra over S st MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) & A is X,S -terms holds
B is X,S -terms
let A, B be non-empty MSAlgebra over S; :: thesis: ( MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) & A is X,S -terms implies B is X,S -terms )
assume A1: MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) ; :: thesis: ( not A is X,S -terms or B is X,S -terms )
assume the Sorts of A is ManySortedSubset of the Sorts of (Free (S,X)) ; :: according to MSAFREE4:def 6 :: thesis: B is X,S -terms
hence the Sorts of B is ManySortedSubset of the Sorts of (Free (S,X)) by A1; :: according to MSAFREE4:def 6 :: thesis: verum