let S1, S2 be non empty ManySortedSign ; 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; 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; ( f,g form_morphism_between S1,S2 implies A | (S1,f,g) is non-empty )
assume
f,g form_morphism_between S1,S2
; 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()
; MSUALG_1:def 3 verum