deffunc H₉( object ) -> set = (In ($1,(the_Vertices_of G))) .degree() ;
consider f being ManySortedSet of the_Vertices_of G such that
A1: for v being object st v in the_Vertices_of G holds
f . v = H₉(v) from PBOOLE:sch 4();
take f ; :: thesis: for v being Vertex of G holds f . v = v .degree()
let v be Vertex of G; :: thesis: f . v = v .degree()
thus f . v = (In (v,(the_Vertices_of G))) .degree() by A1
.= v .degree() ; :: thesis: verum