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
A17: ( k < 0 implies s = {} ) and
A18: ( k = 0 implies s = [:{{} },(0 -polytopes p):] --> (1. Z_2 ) ) and
A19: ( 0 < k & k < dim p implies s = the IncidenceF of p . k ) and
A20: ( k = dim p implies s = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2 ) ) and
A21: ( k > dim p implies s = {} ) and
A22: ( k < 0 implies t = {} ) and
A23: ( k = 0 implies t = [:{{} },(0 -polytopes p):] --> (1. Z_2 ) ) and
A24: ( 0 < k & k < dim p implies t = the IncidenceF of p . k ) and
A25: ( k = dim p implies t = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2 ) ) and
A26: ( 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 A17, A22; :: thesis: verum

end;

suppose k = 0 ; :: thesis: s = t

hence s = t by A18, A23; :: thesis: verum

end;

suppose ( 0 < k & k < dim p ) ; :: thesis: s = t

hence s = t by A19, A24; :: thesis: verum

end;

suppose k = dim p ; :: thesis: s = t

hence s = t by A20, A25; :: thesis: verum

end;

suppose k > dim p ; :: thesis: s = t

hence s = t by A21, A26; :: thesis: verum

end;

end;