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