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

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