set I = the IncidenceF of p;
let s, t be incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p); :: thesis: ( ( k < 0 implies s = {} ) & ( k = 0 implies s = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies s = the IncidenceF of p . k ) & ( k = dim p implies s = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies s = {} ) & ( k < 0 implies t = {} ) & ( k = 0 implies t = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies t = the IncidenceF of p . k ) & ( k = dim p implies t = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies t = {} ) implies s = t )
assume that
A13: ( k < 0 implies s = {} ) and
A14: ( k = 0 implies s = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) and
A15: ( 0 < k & k < dim p implies s = the IncidenceF of p . k ) and
A16: ( k = dim p implies s = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) and
A17: ( k > dim p implies s = {} ) and
( k < 0 implies t = {} ) and
A18: ( k = 0 implies t = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) and
A19: ( 0 < k & k < dim p implies t = the IncidenceF of p . k ) and
A20: ( k = dim p implies t = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) and
( k > dim p implies t = {} ) ; :: thesis: s = t
per cases ( k < 0 or k = 0 or ( 0 < k & k < dim p ) or k = dim p or k > dim p ) by XXREAL_0:1;
suppose k < 0 ; :: thesis: s = t
hence s = t by A13; :: thesis: verum
end;
suppose k = 0 ; :: thesis: s = t
hence s = t by A14, A18; :: thesis: verum
end;
suppose ( 0 < k & k < dim p ) ; :: thesis: s = t
hence s = t by A15, A19; :: thesis: verum
end;
suppose k = dim p ; :: thesis: s = t
hence s = t by A16, A20; :: thesis: verum
end;
suppose k > dim p ; :: thesis: s = t
hence s = t by A17; :: thesis: verum
end;
end;