let S1, S2 be non empty ManySortedSign ; :: thesis: for A, B being MSAlgebra of 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 of 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