let S1, S2 be non void strict ManySortedSign ; ( 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 )
; 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; verum