let S1, S2 be set ; :: thesis: ( ( for u being Term of S,V st u = v holds
S1 = the Sorts of A . (the_sort_of u) ) & ( for u being Term of S,V st u = v holds
S2 = the Sorts of A . (the_sort_of u) ) implies S1 = S2 )
reconsider u = v as Term of S,V by Th4;
assume A1: ( ( for u being Term of S,V st u = v holds
S1 = the Sorts of A . (the_sort_of u) ) & ( for u being Term of S,V st u = v holds
S2 = the Sorts of A . (the_sort_of u) ) & not S1 = S2 ) ; :: thesis: contradiction
then S1 = the Sorts of A . (the_sort_of u) ;
hence contradiction by A1; :: thesis: verum