let G be finite Graph; :: thesis: for v being Vertex of G holds card (Edges_Out v) = EdgesOut v
let v be Vertex of G; :: thesis: card (Edges_Out v) = EdgesOut v
consider X being finite set such that
A1: for z being set holds
( z in X iff ( z in the carrier' of G & the Source of G . z = v ) ) and
A2: EdgesOut v = card X by GRAPH_1:def 22;
now :: thesis: for e being object holds
( e in Edges_Out v iff e in X )
let e be object ; :: thesis: ( e in Edges_Out v iff e in X )
( e in Edges_Out (v, the carrier' of G) iff ( e in the carrier' of G & the Source of G . e = v ) ) by Def2;
hence ( e in Edges_Out v iff e in X ) by A1; :: thesis: verum
end;
hence card (Edges_Out v) = EdgesOut v by A2, TARSKI:2; :: thesis: verum