let S1, S2 be non empty ManySortedSign ; :: thesis: for A, B being MSAlgebra over S2 st MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) holds
for f, g being Function st f,g form_morphism_between S1,S2 holds
A | (S1,f,g) = B | (S1,f,g)
let A, B be MSAlgebra over S2; :: thesis: ( MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) implies for f, g being Function st f,g form_morphism_between S1,S2 holds
A | (S1,f,g) = B | (S1,f,g) )
assume A1: MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) ; :: thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds
A | (S1,f,g) = B | (S1,f,g)
let f, g be Function; :: thesis: ( f,g form_morphism_between S1,S2 implies A | (S1,f,g) = B | (S1,f,g) )
assume A2: f,g form_morphism_between S1,S2 ; :: thesis: A | (S1,f,g) = B | (S1,f,g)
then ( the Sorts of (A | (S1,f,g)) = the Sorts of A * f & the Charact of (A | (S1,f,g)) = the Charact of A * g ) by Def3;
hence A | (S1,f,g) = B | (S1,f,g) by A1, A2, Def3; :: thesis: verum