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
A10: ( (k - 1) -polytopes p is empty implies s = <*> {} ) and
A11: ( 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
A12: ( (k - 1) -polytopes p is empty implies t = <*> {} ) and
A13: ( 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 A10, A12; :: thesis: verum

end;

suppose A14: 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 that
A15: 1 <= n and
A16: 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 A11, A14, A15, A16;
hence s . n = t . n by A11, A13, A14, A15, A16; :: thesis: verum

end;

hence s = t by A11, A13, A14, FINSEQ_1:18; :: thesis: verum

end;

end;