let S be non empty non void ManySortedSign ; :: thesis: for X0 being non-empty countable ManySortedSet of S
for A0 being b₁,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds A0 is Equations (S,A0) -free
let X0 be non-empty countable ManySortedSet of S; :: thesis: for A0 being X0,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds A0 is Equations (S,A0) -free
let A0 be X0,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: A0 is Equations (S,A0) -free
reconsider G = FreeGen X0 as GeneratorSet of A0 by Th45;
take G ; :: according to MSAFREE4:def 13 :: thesis: G is Equations (S,A0) -free
thus G is Equations (S,A0) -free by Th75; :: thesis: verum