let c, d be Element of ((k - 1) -chain-space p); :: thesis: ( ( (k - 1) -polytopes p is empty implies c = 0. ((k - 1) -chain-space p) ) & ( not (k - 1) -polytopes p is empty implies for x being Element of (k - 1) -polytopes p holds
( x in c iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) & ( (k - 1) -polytopes p is empty implies d = 0. ((k - 1) -chain-space p) ) & ( not (k - 1) -polytopes p is empty implies for x being Element of (k - 1) -polytopes p holds
( x in d iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) implies c = d )
assume that
A2: ( (k - 1) -polytopes p is empty implies c = 0. ((k - 1) -chain-space p) ) and
A3: ( not (k - 1) -polytopes p is empty implies for x being Element of (k - 1) -polytopes p holds
( x in c iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) and
( (k - 1) -polytopes p is empty implies d = 0. ((k - 1) -chain-space p) ) and
A4: ( not (k - 1) -polytopes p is empty implies for x being Element of (k - 1) -polytopes p holds
( x in d iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) ; :: thesis: c = d

per cases ( (k - 1) -polytopes p is empty or not (k - 1) -polytopes p is empty ) ;

suppose (k - 1) -polytopes p is empty ; :: thesis: c = d

hence c = d by A2; :: thesis: verum

end;

suppose A5: not (k - 1) -polytopes p is empty ; :: thesis: c = d

for x being Element of (k - 1) -polytopes p holds
( x in c iff x in d )

proof

let x be Element of (k - 1) -polytopes p; :: thesis: ( x in c iff x in d )
thus ( x in c implies x in d ) :: thesis: ( x in d implies x in c )

proof

assume x in c ; :: thesis: x in d
then Sum (incidence-sequence (x,v)) = 1. Z_2 by A3;
hence x in d by A4, A5; :: thesis: verum

end;

thus ( x in d implies x in c ) :: thesis: verum

proof

assume x in d ; :: thesis: x in c
then Sum (incidence-sequence (x,v)) = 1. Z_2 by A4;
hence x in c by A3, A5; :: thesis: verum

end;

end;

hence c = d by Th42; :: thesis: verum

end;

end;