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) --> {} ;
A1: (MCS:Init G) `2 = (the_Vertices_of G) --> {} by MCART_1:def 2;
then dom ((MCS:Init G) `2 ) = the_Vertices_of G by FUNCOP_1:19;
then reconsider f = (the_Vertices_of G) --> {} as PartFunc of (the_Vertices_of G),(rng ((the_Vertices_of G) --> {} )) by A1, RELSET_1:11;

now

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:13; :: thesis: verum

end;

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

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

end;

end;

end;

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