consider x being object such that
A2: x in dom the ResultSort of IIG and
A3: the ResultSort of IIG . x = v by A1, FUNCT_1:def 3;
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 A3; :: thesis: verum