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