let S1, S2 be non empty ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over 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 over 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 V2() ; :: according to MSUALG_1:def 3 :: thesis: verum

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 over 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 V2() ; :: according to MSUALG_1:def 3 :: thesis: verum