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, FINSEQ_1:18; :: thesis: verum

end;

end;