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 by FUNCOP_1:13;
then reconsider f = (the_Vertices_of G) --> {} as PartFunc of (the_Vertices_of G),(rng ((the_Vertices_of G) --> {})) by RELSET_1:4;

now :: thesis: for x being set holds f . x = {}

let x be set ; :: thesis: f . b₁ = {}

per cases ( x in dom f or not x in dom f ) ;

suppose x in dom f ; :: thesis: f . b₁ = {}

hence f . x = {} by FUNCOP_1:7; :: thesis: verum

end;

suppose not x in dom f ; :: thesis: f . b₁ = {}

hence f . x = {} by FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

hence ((MCS:Init G) `2) . v = 0 ; :: thesis: verum