let U1, U2 be Universal_Algebra; :: thesis: ( U1 is SubAlgebra of U2 implies MSSign U1 = MSSign U2 )
set ff2 = (dom (signature U1)) --> z;
set gg2 = (dom (signature U2)) --> z;
reconsider ff1 = (*--> 0) * (signature U1) as Function of (dom (signature U1)),({0} *) by MSUALG_1:2;
reconsider gg1 = (*--> 0) * (signature U2) as Function of (dom (signature U2)),({0} *) by MSUALG_1:2;
assume U1 is SubAlgebra of U2 ; :: thesis: MSSign U1 = MSSign U2
then A1: U1,U2 are_similar by UNIALG_2:13;
A2: ( MSSign U1 = ManySortedSign(# {0},(dom (signature U1)),ff1,((dom (signature U1)) --> z) #) & MSSign U2 = ManySortedSign(# {0},(dom (signature U2)),gg1,((dom (signature U2)) --> z) #) ) by MSUALG_1:10;
thus MSSign U1 = MSSign U2 by A1, A2; :: thesis: verum