consider x being set such that
A2: ( x in dom the ResultSort of IIG & the ResultSort of IIG . x = v ) by A1, FUNCT_1:def 5;
reconsider x = x as OperSymbol of IIG by A2;
take x ; :: thesis: the_result_sort_of x = v
thus the_result_sort_of x = v by A2; :: thesis: verum