deffunc H₉( object ) -> set = (In ($1,(the_Vertices_of G))) .outDegree() ;
consider f being ManySortedSet of the_Vertices_of G such that
A7: 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 .outDegree()
let v be Vertex of G; :: thesis: f . v = v .outDegree()
thus f . v = (In (v,(the_Vertices_of G))) .outDegree() by A7
.= v .outDegree() ; :: thesis: verum