let S1, S2 be void strict ManySortedSign ; :: thesis: ( the carrier of S1 = {x} & the carrier of S2 = {x} implies S1 = S2 )
assume that
A1: the carrier of S1 = {x} and
A2: the carrier of S2 = {x} ; :: thesis: S1 = S2
the Arity of S1 = the Arity of S2 ;
hence S1 = S2 by A1, A2; :: thesis: verum