let B be non empty non void ManySortedSign ; :: thesis: for T, C being non-empty MSAlgebra over B
for X being non-empty 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 non-empty 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 non-empty 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