let s, t be FinSequence of Z_2; :: thesis: ( ( (k - 1) -polytopes p is empty implies s = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len s = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
s . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) & ( (k - 1) -polytopes p is empty implies t = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len t = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
t . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) implies s = t )
assume that
A6: ( (k - 1) -polytopes p is empty implies s = <*> {} ) and
A7: ( not (k - 1) -polytopes p is empty implies ( len s = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
s . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) and
A8: ( (k - 1) -polytopes p is empty implies t = <*> {} ) and
A9: ( not (k - 1) -polytopes p is empty implies ( len t = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
t . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) ; :: thesis: s = t

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

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

hence s = t by A6, A8; :: thesis: verum

end;

suppose A10: not (k - 1) -polytopes p is empty ; :: thesis: s = t

for n being Nat st 1 <= n & n <= len s holds
s . n = t . n

proof

let n be Nat; :: thesis: ( 1 <= n & n <= len s implies s . n = t . n )
assume A11: ( 1 <= n & n <= len s ) ; :: thesis: s . n = t . n
reconsider n = n as Nat ;
s . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) by A7, A10, A11;
hence s . n = t . n by A7, A9, A10, A11; :: thesis: verum

end;

hence s = t by A7, A9, A10; :: thesis: verum

end;

end;