let B be non empty non void ManySortedSign ; :: thesis: for T, C being non-empty MSAlgebra over B

for X being V2() GeneratorSet of T

for g being set st g in C -States X holds

g is ManySortedFunction of X, the Sorts of C

let T, C be non-empty MSAlgebra over B; :: thesis: for X being V2() GeneratorSet of T

for g being set st g in C -States X holds

g is ManySortedFunction of X, the Sorts of C

let X be V2() GeneratorSet of T; :: thesis: for g being set st g in C -States X holds

g is ManySortedFunction of X, the Sorts of C

X is_transformable_to the Sorts of C ;

hence for g being set st g in C -States X holds

g is ManySortedFunction of X, the Sorts of C by AUTALG_1:19; :: thesis: verum

for X being V2() GeneratorSet of T

for g being set st g in C -States X holds

g is ManySortedFunction of X, the Sorts of C

let T, C be non-empty MSAlgebra over B; :: thesis: for X being V2() GeneratorSet of T

for g being set st g in C -States X holds

g is ManySortedFunction of X, the Sorts of C

let X be V2() GeneratorSet of T; :: thesis: for g being set st g in C -States X holds

g is ManySortedFunction of X, the Sorts of C

X is_transformable_to the Sorts of C ;

hence for g being set st g in C -States X holds

g is ManySortedFunction of X, the Sorts of C by AUTALG_1:19; :: thesis: verum