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;