let f1, f2 be ManySortedSet of the_Vertices_of G; :: thesis: ( ( for v being Vertex of G holds f1 . v = v .outDegree() ) & ( for v being Vertex of G holds f2 . v = v .outDegree() ) implies f1 = f2 )
assume that
A8: for v being Vertex of G holds f1 . v = v .outDegree() and
A9: for v being Vertex of G holds f2 . v = v .outDegree() ; :: thesis: f1 = f2

now :: thesis: for v being object st v in the_Vertices_of G holds
f1 . v = f2 . v

let v be object ; :: thesis: ( v in the_Vertices_of G implies f1 . v = f2 . v )
assume v in the_Vertices_of G ; :: thesis: f1 . v = f2 . v
then reconsider v0 = v as Vertex of G ;
thus f1 . v = v0 .outDegree() by A8
.= f2 . v by A9 ; :: thesis: verum

end;

hence f1 = f2 by PBOOLE:3; :: thesis: verum