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