let S1, S2 be non void strict ManySortedSign ; :: thesis: ( the carrier of S1 = (rng p) \/ {x} & the carrier' of S1 = {[p,f]} & the Arity of S1 . [p,f] = p & the ResultSort of S1 . [p,f] = x & the carrier of S2 = (rng p) \/ {x} & the carrier' of S2 = {[p,f]} & the Arity of S2 . [p,f] = p & the ResultSort of S2 . [p,f] = x implies S1 = S2 )
assume A1: ( the carrier of S1 = (rng p) \/ {x} & the carrier' of S1 = {[p,f]} & the Arity of S1 . [p,f] = p & the ResultSort of S1 . [p,f] = x & the carrier of S2 = (rng p) \/ {x} & the carrier' of S2 = {[p,f]} & the Arity of S2 . [p,f] = p & the ResultSort of S2 . [p,f] = x & not S1 = S2 ) ; :: thesis: contradiction
then dom the Arity of S1 = {[p,f]} by FUNCT_2:def 1;
then A2: the Arity of S1 = {[[p,f],p]} by A1, GRFUNC_1:7;
dom the ResultSort of S1 = {[p,f]} by A1, FUNCT_2:def 1;
then A3: the ResultSort of S1 = {[[p,f],x]} by A1, GRFUNC_1:7;
dom the Arity of S2 = {[p,f]} by A1, FUNCT_2:def 1;
then A4: the Arity of S2 = {[[p,f],p]} by A1, GRFUNC_1:7;
dom the ResultSort of S2 = {[p,f]} by A1, FUNCT_2:def 1;
hence contradiction by A1, A2, A4, A3, GRFUNC_1:7; :: thesis: verum