let p be polyhedron; :: thesis: ( p is simply-connected implies p is eulerian )
assume A1: p is simply-connected ; :: thesis: p is eulerian
set apcs = alternating-proper-f-vector p;

per cases ( dim p = 0 or dim p > 0 ) ;

suppose dim p = 0 ; :: thesis: p is eulerian

hence p is eulerian by Th85; :: thesis: verum

end;

suppose A2: dim p > 0 ; :: thesis: p is eulerian

deffunc H₁( Nat) -> set = ((- 1) |^ ($1 + 1)) * (dim (($1 - 1) -circuit-space p));
deffunc H₂( Nat) -> set = ((- 1) |^ ($1 + 1)) * (dim (($1 - 2) -bounding-chain-space p));
consider a being FinSequence such that
A3: len a = len (alternating-proper-f-vector p) and
A4: for n being Nat st n in dom a holds
a . n = H₂(n) from FINSEQ_1:sch 2();
A5: rng a c= INT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng a or y in INT )
assume y in rng a ; :: thesis: y in INT
then consider x being object such that
A6: x in dom a and
A7: y = a . x by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A6;
a . x = ((- 1) |^ (x + 1)) * (dim ((x - 2) -bounding-chain-space p)) by A4, A6;
hence y in INT by A7, INT_1:def 2; :: thesis: verum

end;

consider b being FinSequence such that
A8: len b = len (alternating-proper-f-vector p) and
A9: for n being Nat st n in dom b holds
b . n = H₁(n) from FINSEQ_1:sch 2();
rng b c= INT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng b or y in INT )
assume y in rng b ; :: thesis: y in INT
then consider x being object such that
A10: x in dom b and
A11: y = b . x by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A10;
b . x = ((- 1) |^ (x + 1)) * (dim ((x - 1) -circuit-space p)) by A9, A10;
hence y in INT by A11, INT_1:def 2; :: thesis: verum

end;

then reconsider a = a, b = b as FinSequence of INT by A5, FINSEQ_1:def 4;
A12: len (alternating-proper-f-vector p) > 0 by A2, Def27;
A13: a . 1 = 1

proof

reconsider egy = 1 as Element of NAT ;
1 <= 0 + 1 ;
then egy <= len (alternating-proper-f-vector p) by A12, NAT_1:13;
then egy in dom a by A3, FINSEQ_3:25;
then a . egy = ((- 1) |^ (1 + 1)) * (dim ((egy - 2) -bounding-chain-space p)) by A4
.= 1 * (dim ((egy - 2) -bounding-chain-space p)) by Th4, Th7
.= 1 by Th60 ;
hence a . 1 = 1 ; :: thesis: verum

end;

A14: for n being Nat st 1 <= n & n < len (alternating-proper-f-vector p) holds
b . n = - (a . (n + 1))

proof

let n be Nat; :: thesis: ( 1 <= n & n < len (alternating-proper-f-vector p) implies b . n = - (a . (n + 1)) )
assume that
A15: 1 <= n and
A16: n < len (alternating-proper-f-vector p) ; :: thesis: b . n = - (a . (n + 1))
A17: n in dom b by A8, A15, A16, FINSEQ_3:25;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A18: b . n = ((- 1) |^ (n + 1)) * (dim ((n - 1) -circuit-space p)) by A9, A17;
A19: 1 <= n + 1 by NAT_1:11;
n + 1 <= len (alternating-proper-f-vector p) by A16, INT_1:7;
then n + 1 in dom a by A3, A19, FINSEQ_3:25;
then a . (n + 1) = H₂(n + 1) by A4
.= (((- 1) |^ (n + 1)) * ((- 1) |^ 1)) * (dim ((n - 1) -bounding-chain-space p)) by NEWTON:8
.= (((- 1) |^ (n + 1)) * (- 1)) * (dim ((n - 1) -bounding-chain-space p))
.= - (((- 1) |^ (n + 1)) * (dim ((n - 1) -bounding-chain-space p)))
.= - (b . n) by A1, A18, Th48 ;
hence b . n = - (a . (n + 1)) ; :: thesis: verum

end;

A20: b . (len (alternating-proper-f-vector p)) = (- 1) |^ ((dim p) + 1)

proof

reconsider n = len (alternating-proper-f-vector p) as Element of NAT ;
A21: n = dim p by Def27;
0 + 1 = 1 ;
then 1 <= len (alternating-proper-f-vector p) by A12, NAT_1:13;
then n in dom b by A8, FINSEQ_3:25;
then b . n = H₁(n) by A9
.= ((- 1) |^ (n + 1)) * 1 by A1, A21, Th77
.= (- 1) |^ (n + 1) ;
hence b . (len (alternating-proper-f-vector p)) = (- 1) |^ ((dim p) + 1) by Def27; :: thesis: verum

end;

for n being Nat st 1 <= n & n <= len (alternating-proper-f-vector p) holds
(alternating-proper-f-vector p) . n = (a . n) + (b . n)

proof

let n be Nat; :: thesis: ( 1 <= n & n <= len (alternating-proper-f-vector p) implies (alternating-proper-f-vector p) . n = (a . n) + (b . n) )
assume A22: ( 1 <= n & n <= len (alternating-proper-f-vector p) ) ; :: thesis: (alternating-proper-f-vector p) . n = (a . n) + (b . n)
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
n9 in dom a by A3, A22, FINSEQ_3:25;
then A23: a . n9 = ((- 1) |^ (n9 + 1)) * (dim ((n9 - 2) -bounding-chain-space p)) by A4;
( (alternating-proper-f-vector p) . n = (((- 1) |^ (n + 1)) * (dim ((n - 2) -bounding-chain-space p))) + (((- 1) |^ (n + 1)) * (dim ((n - 1) -circuit-space p))) & n9 in dom b ) by A8, A22, Th49, FINSEQ_3:25;
hence (alternating-proper-f-vector p) . n = (a . n) + (b . n) by A9, A23; :: thesis: verum

end;

then Sum (alternating-proper-f-vector p) = (a . 1) + (b . (len (alternating-proper-f-vector p))) by A12, A3, A8, A14, Th13;
hence p is eulerian by A13, A20; :: thesis: verum

end;

end;