let G be non empty non void ManySortedSign ; :: thesis: for v being Vertex of G st v in InputVertices G holds
for o being OperSymbol of G holds not the_result_sort_of o = v
let v be Vertex of G; :: thesis: ( v in InputVertices G implies for o being OperSymbol of G holds not the_result_sort_of o = v )
assume A1: v in InputVertices G ; :: thesis: for o being OperSymbol of G holds not the_result_sort_of o = v
let o be OperSymbol of G; :: thesis: not the_result_sort_of o = v
assume A2: the_result_sort_of o = v ; :: thesis: contradiction
o in the carrier' of G ;
then o in dom the ResultSort of G by FUNCT_2:def 1;
then v in rng the ResultSort of G by A2, FUNCT_1:def 3;
hence contradiction by A1, XBOOLE_0:def 5; :: thesis: verum