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

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