let G be finite _Graph; :: thesis: for v being set holds ((MCS:Init G) `2) . v = 0
let v be set ; :: thesis: ((MCS:Init G) `2) . v = 0
set g = (the_Vertices_of G) --> {};
dom ((MCS:Init G) `2) = the_Vertices_of G ;
then reconsider f = (the_Vertices_of G) --> {} as PartFunc of (the_Vertices_of G),(rng ((the_Vertices_of G) --> {})) by RELSET_1:4;
thus ((MCS:Init G) `2) . v = 0 ; :: thesis: verum