set A = the X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

consider VF being ManySortedMSSet of the Sorts of the X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S, the Sorts of the X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S, B being X,S -terms all_vars_including inheriting_operations free_in_itself VarMSAlgebra over S such that

A1: ( B = VarMSAlgebra(# the Sorts of the X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S, the Charact of the X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S,VF #) & B is vf-free ) by Th34;

take B ; :: thesis: ( B is strict & B is vf-free )

thus ( B is strict & B is vf-free ) by A1; :: thesis: verum

consider VF being ManySortedMSSet of the Sorts of the X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S, the Sorts of the X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S, B being X,S -terms all_vars_including inheriting_operations free_in_itself VarMSAlgebra over S such that

A1: ( B = VarMSAlgebra(# the Sorts of the X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S, the Charact of the X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S,VF #) & B is vf-free ) by Th34;

take B ; :: thesis: ( B is strict & B is vf-free )

thus ( B is strict & B is vf-free ) by A1; :: thesis: verum