let f1, f2 be ManySortedSet of the_Vertices_of G; :: thesis: ( ( for v being Vertex of G holds f1 . v = v .degree() ) & ( for v being Vertex of G holds f2 . v = v .degree() ) implies f1 = f2 )
assume that
A2: for v being Vertex of G holds f1 . v = v .degree() and
A3: for v being Vertex of G holds f2 . v = v .degree() ; :: 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 .degree() by A2
.= f2 . v by A3 ; :: thesis: verum

end;

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