let S1, S2 be non empty ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S2
for f, g being Function st f,g form_morphism_between S1,S2 holds
A | S1,f,g is non-empty
let A be non-empty MSAlgebra of S2; :: thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds
A | S1,f,g is non-empty
let f, g be Function; :: thesis: ( f,g form_morphism_between S1,S2 implies A | S1,f,g is non-empty )
assume f,g form_morphism_between S1,S2 ; :: thesis: A | S1,f,g is non-empty
then the Sorts of (A | S1,f,g) = the Sorts of A * f by Def3;
hence the Sorts of (A | S1,f,g) is non-empty ; :: according to MSUALG_1:def 8 :: thesis: verum