let G be _finite _Graph; for k being Nat st k = card { w where w is Vertex of G : not w .degree() is even } holds
k is even
let k be Nat; ( k = card { w where w is Vertex of G : not w .degree() is even } implies k is even )
set W = { w where w is Vertex of G : not w .degree() is even } ;
assume A1:
k = card { w where w is Vertex of G : not w .degree() is even }
; k is even
then A3:
{ w where w is Vertex of G : not w .degree() is even } c= the_Vertices_of G
by TARSKI:def 3;
set v = the Denumeration of (the_Vertices_of G);
reconsider v9 = { w where w is Vertex of G : not w .degree() is even } |` the Denumeration of (the_Vertices_of G) as one-to-one Function by FUNCT_1:58;
set f = v9 " ;
deffunc H9( Nat) -> Element of omega = (((G .degreeMap()) * the Denumeration of (the_Vertices_of G)) . $1) mod 2;
consider m being XFinSequence of NAT such that
A4:
len m = len ((G .degreeMap()) * the Denumeration of (the_Vertices_of G))
and
A5:
for k being Nat st k in len ((G .degreeMap()) * the Denumeration of (the_Vertices_of G)) holds
m . k = H9(k)
from AFINSQ_2:sch 1();
A6:
( dom ((G .degreeMap()) * the Denumeration of (the_Vertices_of G)) = dom m & ( for i being Nat st i in dom ((G .degreeMap()) * the Denumeration of (the_Vertices_of G)) holds
m . i = (((G .degreeMap()) * the Denumeration of (the_Vertices_of G)) . i) mod 2 ) )
by A4, A5;
A7: dom (v9 ") =
rng v9
by FUNCT_1:33
.=
(rng the Denumeration of (the_Vertices_of G)) /\ { w where w is Vertex of G : not w .degree() is even }
by RELAT_1:88
.=
(the_Vertices_of G) /\ { w where w is Vertex of G : not w .degree() is even }
by FUNCT_2:def 3
.=
{ w where w is Vertex of G : not w .degree() is even }
by A3, XBOOLE_1:28
;
now for y being object holds
( ( y in m " {1} implies ex x being object st
( x in dom (v9 ") & y = (v9 ") . x ) ) & ( ex x being object st
( x in dom (v9 ") & y = (v9 ") . x ) implies y in m " {1} ) )let y be
object ;
( ( y in m " {1} implies ex x being object st
( x in dom (v9 ") & y = (v9 ") . x ) ) & ( ex x being object st
( x in dom (v9 ") & y = (v9 ") . x ) implies y in m " {1} ) )hereby ( ex x being object st
( x in dom (v9 ") & y = (v9 ") . x ) implies y in m " {1} )
assume
y in m " {1}
;
ex x being object st
( x in dom (v9 ") & y = (v9 ") . x )then A8:
(
y in dom m &
m . y in {1} )
by FUNCT_1:def 7;
reconsider x = the
Denumeration of
(the_Vertices_of G) . y as
object ;
take x =
x;
( x in dom (v9 ") & y = (v9 ") . x )A9:
y in dom the
Denumeration of
(the_Vertices_of G)
by A4, A8, FUNCT_1:11;
1 =
m . y
by A8, TARSKI:def 1
.=
(((G .degreeMap()) * the Denumeration of (the_Vertices_of G)) . y) mod 2
by A8, A4, A5
.=
((G .degreeMap()) . ( the Denumeration of (the_Vertices_of G) . y)) mod 2
by A9, FUNCT_1:13
.=
((G .degreeMap()) . ( the Denumeration of (the_Vertices_of G) /. y)) mod 2
by A9, PARTFUN1:def 6
.=
(( the Denumeration of (the_Vertices_of G) /. y) .degree()) mod 2
by Def11
;
then
not
( the Denumeration of (the_Vertices_of G) /. y) .degree() is
even
by NAT_2:21;
then
the
Denumeration of
(the_Vertices_of G) /. y in { w where w is Vertex of G : not w .degree() is even }
;
then A10:
x in { w where w is Vertex of G : not w .degree() is even }
by A9, PARTFUN1:def 6;
x in rng the
Denumeration of
(the_Vertices_of G)
by A9, FUNCT_1:3;
then
x in rng v9
by A10, RELAT_1:84;
hence
x in dom (v9 ")
by FUNCT_1:33;
y = (v9 ") . xthus y =
( the Denumeration of (the_Vertices_of G) ") . x
by A9, FUNCT_1:34
.=
(( the Denumeration of (the_Vertices_of G) ") | { w where w is Vertex of G : not w .degree() is even } ) . x
by A10, FUNCT_1:49
.=
(v9 ") . x
by GLIB_009:5
;
verum
end; given x being
object such that A11:
(
x in dom (v9 ") &
y = (v9 ") . x )
;
y in m " {1}
x in rng v9
by A11, FUNCT_1:33;
then A12:
(
x in rng the
Denumeration of
(the_Vertices_of G) &
x in { w where w is Vertex of G : not w .degree() is even } )
by RELAT_1:84;
then consider w being
Vertex of
G such that A13:
(
x = w & not
w .degree() is
even )
;
A14:
x in dom ( the Denumeration of (the_Vertices_of G) ")
by A12, FUNCT_1:33;
A15:
y =
(( the Denumeration of (the_Vertices_of G) ") | { w where w is Vertex of G : not w .degree() is even } ) . x
by A11, GLIB_009:5
.=
( the Denumeration of (the_Vertices_of G) ") . x
by A12, FUNCT_1:49
;
then
y in rng ( the Denumeration of (the_Vertices_of G) ")
by A14, FUNCT_1:3;
then A16:
y in dom the
Denumeration of
(the_Vertices_of G)
by FUNCT_1:33;
A17:
the
Denumeration of
(the_Vertices_of G) . y = x
by A12, A15, FUNCT_1:35;
x in the_Vertices_of G
by A13;
then
x in dom (G .degreeMap())
by PARTFUN1:def 2;
then A18:
y in dom m
by A4, A16, A17, FUNCT_1:11;
then m . y =
(((G .degreeMap()) * the Denumeration of (the_Vertices_of G)) . y) mod 2
by A4, A5
.=
((G .degreeMap()) . x) mod 2
by A16, A17, FUNCT_1:13
.=
(w .degree()) mod 2
by A13, Def11
.=
1
by A13, NAT_2:22
;
then
m . y in {1}
by TARSKI:def 1;
hence
y in m " {1}
by A18, FUNCT_1:def 7;
verum end;
then A19:
rng (v9 ") = m " {1}
by FUNCT_1:def 3;
then A22:
rng m c= {0,1}
by TARSKI:def 3;
k =
1 * (card (m " {1}))
by A1, A7, A19, CARD_1:70
.=
Sum m
by A22, AFINSQ_2:68
;
then k mod 2 =
(Sum ((G .degreeMap()) * the Denumeration of (the_Vertices_of G))) mod 2
by A6, NUMERAL1:3
.=
(2 * (G .size())) mod 2
by Th66
.=
0
by NAT_D:13
;
hence
k is even
by NAT_2:21; verum