let c, d be Element of ((k - 1) -chain-space p); :: thesis:
assume that
A4: ( (k - 1) -polytopes p is empty implies c = 0. ((k - 1) -chain-space p) ) and
A5: ( 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
A7: ( 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:

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

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

hence c = d by A4; :: thesis:

end;

suppose A8: not (k - 1) -polytopes p is empty ; :: thesis:

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:
thus ( x in c implies x in d ) :: thesis:

proof

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

end;

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

proof

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

end;

end;

hence c = d by Th45; :: thesis:

end;

end;