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 A2: ( 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]} & dom the Arity of S2 = {[p,f]} & dom the ResultSort of S1 = {[p,f]} & dom the ResultSort of S2 = {[p,f]} ) by FUNCT_2:def 1;
then ( the Arity of S1 = {[[p,f],p]} & the Arity of S2 = {[[p,f],p]} & the ResultSort of S1 = {[[p,f],x]} & the ResultSort of S2 = {[[p,f],x]} ) by A2, GRFUNC_1:18;
hence contradiction by A2; :: thesis: verum