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