let U1, U2 be Universal_Algebra; :: thesis: ( U1,U2 are_similar implies MSSign U1 = MSSign U2 )
assume A1: U1,U2 are_similar ; :: thesis: MSSign U1 = MSSign U2
reconsider f = (*--> 0) * (signature U1) as Function of (dom (signature U1)),({0} *) by MSUALG_1:2;
A2: ( the carrier of (MSSign U1) = {0} & the Arity of (MSSign U1) = f ) by MSUALG_1:def 8;
reconsider f = (*--> 0) * (signature U2) as Function of (dom (signature U2)),({0} *) by MSUALG_1:2;
A3: ( the Arity of (MSSign U2) = f & the ResultSort of (MSSign U2) = (dom (signature U2)) --> 0 ) by MSUALG_1:def 8;
A4: ( the ResultSort of (MSSign U1) = (dom (signature U1)) --> 0 & the carrier of (MSSign U2) = {0} ) by MSUALG_1:def 8;
( the carrier' of (MSSign U1) = dom (signature U1) & the carrier' of (MSSign U2) = dom (signature U2) ) by MSUALG_1:def 8;
then the carrier' of (MSSign U1) = the carrier' of (MSSign U2) by A1;
hence MSSign U1 = MSSign U2 by A1, A2, A4, A3; :: thesis: verum