per cases ( k < 0 or k > dim p or ( 0 < k & k < dim p ) or k = 0 or k = dim p ) by XXREAL_0:1;

suppose A1: k < 0 ; :: thesis: ex b₁ being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) st
( ( k < 0 implies b₁ = {} ) & ( k = 0 implies b₁ = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b₁ = the IncidenceF of p . k ) & ( k = dim p implies b₁ = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b₁ = {} ) )

set f = {} ;
reconsider f = {} as Function ;
k - 1 < 0 - 1 by A1, XREAL_1:9;
then (k - 1) -polytopes p = {} by Def5;
then [:((k - 1) -polytopes p),(k -polytopes p):] = {} by ZFMISC_1:90;
then reconsider f = f as Function of [:((k - 1) -polytopes p),(k -polytopes p):],{(0. Z_2),(1. Z_2)} by RELSET_1:12;
reconsider f = f as Element of Funcs ([:((k - 1) -polytopes p),(k -polytopes p):],{(0. Z_2),(1. Z_2)}) by FUNCT_2:8;
take f ; :: thesis: ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) )
thus ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) ) by A1; :: thesis: verum

end;

suppose A2: k > dim p ; :: thesis: ex b₁ being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) st
( ( k < 0 implies b₁ = {} ) & ( k = 0 implies b₁ = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b₁ = the IncidenceF of p . k ) & ( k = dim p implies b₁ = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b₁ = {} ) )

set f = {} ;
reconsider f = {} as Function ;
k -polytopes p = {} by A2, Th23;
then [:((k - 1) -polytopes p),(k -polytopes p):] = {} by ZFMISC_1:90;
then reconsider f = f as Function of [:((k - 1) -polytopes p),(k -polytopes p):],{(0. Z_2),(1. Z_2)} by RELSET_1:12;
reconsider f = f as Element of Funcs ([:((k - 1) -polytopes p),(k -polytopes p):],{(0. Z_2),(1. Z_2)}) by FUNCT_2:8;
take f ; :: thesis: ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) )
thus ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) ) by A2; :: thesis: verum

end;

suppose A3: ( 0 < k & k < dim p ) ; :: thesis: ex b₁ being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) st
( ( k < 0 implies b₁ = {} ) & ( k = 0 implies b₁ = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b₁ = the IncidenceF of p . k ) & ( k = dim p implies b₁ = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b₁ = {} ) )

set F = the PolytopsF of p;
set I = the IncidenceF of p;
A4: k -polytopes p = rng ( the PolytopsF of p . (k + 1)) by A3, Def5;
A5: k - 1 < dim p by A3, XREAL_1:146, XXREAL_0:2;
0 + 1 = 1 ;
then A6: 1 <= k by A3, INT_1:7;
then reconsider k9 = k as Nat by Th2;
1 - 1 = 0 ;
then - 1 < k - 1 by A6, XREAL_1:9;
then (k - 1) -polytopes p = rng ( the PolytopsF of p . ((k - 1) + 1)) by A5, Def5;
then reconsider Ik = the IncidenceF of p . k9 as incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) by A3, A6, A4, Def2;
take Ik ; :: thesis: ( ( k < 0 implies Ik = {} ) & ( k = 0 implies Ik = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies Ik = the IncidenceF of p . k ) & ( k = dim p implies Ik = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies Ik = {} ) )
thus ( ( k < 0 implies Ik = {} ) & ( k = 0 implies Ik = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies Ik = the IncidenceF of p . k ) & ( k = dim p implies Ik = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies Ik = {} ) ) by A3; :: thesis: verum

end;

suppose A7: k = 0 ; :: thesis: ex b₁ being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) st
( ( k < 0 implies b₁ = {} ) & ( k = 0 implies b₁ = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b₁ = the IncidenceF of p . k ) & ( k = dim p implies b₁ = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b₁ = {} ) )

per cases ( k = dim p or k <> dim p ) ;

suppose A8: k = dim p ; :: thesis: ex b₁ being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) st
( ( k < 0 implies b₁ = {} ) & ( k = 0 implies b₁ = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b₁ = the IncidenceF of p . k ) & ( k = dim p implies b₁ = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b₁ = {} ) )

set f = [:{{}},{p}:] --> (1. Z_2);
reconsider f = [:{{}},{p}:] --> (1. Z_2) as incidence-matrix of {{}},{p} by Th21;
(k - 1) -polytopes p = {{}} by A7, Def5;
then reconsider f = f as incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) by A8, Def5;
take f ; :: thesis: ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) )
thus ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) ) by A7, A8, Def5; :: thesis: verum

end;

suppose A9: k <> dim p ; :: thesis: ex b₁ being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) st
( ( k < 0 implies b₁ = {} ) & ( k = 0 implies b₁ = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b₁ = the IncidenceF of p . k ) & ( k = dim p implies b₁ = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b₁ = {} ) )

set f = [:{{}},(0 -polytopes p):] --> (1. Z_2);
reconsider f = [:{{}},(0 -polytopes p):] --> (1. Z_2) as incidence-matrix of {{}},(0 -polytopes p) by Th21;
reconsider f = f as incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) by A7, Def5;
take f ; :: thesis: ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) )
thus ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) ) by A7, A9; :: thesis: verum

end;

end;

end;

suppose A10: k = dim p ; :: thesis: ex b₁ being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) st
( ( k < 0 implies b₁ = {} ) & ( k = 0 implies b₁ = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b₁ = the IncidenceF of p . k ) & ( k = dim p implies b₁ = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b₁ = {} ) )

per cases ( k = 0 or k <> 0 ) ;

suppose A11: k = 0 ; :: thesis: ex b₁ being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) st
( ( k < 0 implies b₁ = {} ) & ( k = 0 implies b₁ = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b₁ = the IncidenceF of p . k ) & ( k = dim p implies b₁ = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b₁ = {} ) )

set f = [:{{}},{p}:] --> (1. Z_2);
reconsider f = [:{{}},{p}:] --> (1. Z_2) as incidence-matrix of {{}},{p} by Th21;
(k - 1) -polytopes p = {{}} by A11, Def5;
then reconsider f = f as incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) by A10, Def5;
take f ; :: thesis: ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) )
thus ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) ) by A10, A11, Def5; :: thesis: verum

end;

suppose A12: k <> 0 ; :: thesis: ex b₁ being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) st
( ( k < 0 implies b₁ = {} ) & ( k = 0 implies b₁ = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b₁ = the IncidenceF of p . k ) & ( k = dim p implies b₁ = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b₁ = {} ) )

set f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2);
reconsider f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) as incidence-matrix of (((dim p) - 1) -polytopes p),{p} by Th21;
reconsider f = f as incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) by A10, Def5;
take f ; :: thesis: ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) )
thus ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) ) by A10, A12; :: thesis: verum

end;

end;

end;

end;