let G2 be _Graph; :: thesis: for V being Subset of (the_Vertices_of G2)
for G1 being addLoops of G2,V holds G1 .size() = (G2 .size()) +` (card V)
let V be Subset of (the_Vertices_of G2); :: thesis: for G1 being addLoops of G2,V holds G1 .size() = (G2 .size()) +` (card V)
let G1 be addLoops of G2,V; :: thesis: G1 .size() = (G2 .size()) +` (card V)
consider E being set , f being one-to-one Function such that
A1: ( E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & dom f = E & rng f = V & the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* f ) by Def5;
thus G1 .size() = (card (the_Edges_of G2)) +` (card E) by A1, CARD_2:35
.= (G2 .size()) +` (card V) by A1, CARD_1:70 ; :: thesis: verum