for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S
for A being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S ex VF being ManySortedMSSet of the Sorts of A, the Sorts of A ex B being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself VarMSAlgebra over S st
( B = VarMSAlgebra(# the Sorts of A, the Charact of A,VF #) & B is vf-free )