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₁ = {} ) )

(k - 1) -polytopes p = {}

proof

k - 1 < 0 - 1 by A1, XREAL_1:11;
hence (k - 1) -polytopes p = {} by Th26; :: thesis: verum

end;

then A2: [:((k - 1) -polytopes p),(k -polytopes p):] = {} by ZFMISC_1:113;
set f = {} ;
reconsider f = {} as Function ;
reconsider f = f as Function of [:((k - 1) -polytopes p),(k -polytopes p):],{(0. Z_2 ),(1. Z_2 )} by A2, RELSET_1:25;
reconsider f = f as Element of Funcs [:((k - 1) -polytopes p),(k -polytopes p):],{(0. Z_2 ),(1. Z_2 )} by FUNCT_2:11;
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 A3: 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₁ = {} ) )

then k -polytopes p = {} by Th26;
then A4: [:((k - 1) -polytopes p),(k -polytopes p):] = {} by ZFMISC_1:113;
set f = {} ;
reconsider f = {} as Function ;
reconsider f = f as Function of [:((k - 1) -polytopes p),(k -polytopes p):],{(0. Z_2 ),(1. Z_2 )} by A4, RELSET_1:25;
reconsider f = f as Element of Funcs [:((k - 1) -polytopes p),(k -polytopes p):],{(0. Z_2 ),(1. Z_2 )} by FUNCT_2:11;
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 A3; :: thesis: verum

end;

suppose A5: ( 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;
0 + 1 = 1 ;
then A6: 1 <= k by A5, INT_1:20;
1 - 1 = 0 ;
then ( - 1 < k - 1 & k - 1 < dim p ) by A5, A6, Th27, XREAL_1:11;
then A7: (k - 1) -polytopes p = rng (the PolytopsF of p . ((k - 1) + 1)) by Def5;
A8: k -polytopes p = rng (the PolytopsF of p . (k + 1)) by A5, Def5;
reconsider k' = k as Nat by A6, Th3;
reconsider Ik = the IncidenceF of p . k' as incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) by A5, A6, A7, A8, 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 A5; :: thesis: verum

end;

suppose A9: 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 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₁ = {} ) )

A11: (k - 1) -polytopes p = {{} } by A9, Def5;
set f = [:{{} },{p}:] --> (1. Z_2 );
reconsider f = [:{{} },{p}:] --> (1. Z_2 ) as incidence-matrix of {{} },{p} by Th24;
reconsider f = f as incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) by A10, A11, 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 A9, A10, Def5; :: thesis: verum

end;

suppose A12: 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 Th24;
reconsider f = f as incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) by A9, 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 A9, A12; :: thesis: verum

end;

end;

end;

suppose A13: 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 A14: 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₁ = {} ) )

then A15: (k - 1) -polytopes p = {{} } by Def5;
set f = [:{{} },{p}:] --> (1. Z_2 );
reconsider f = [:{{} },{p}:] --> (1. Z_2 ) as incidence-matrix of {{} },{p} by Th24;
reconsider f = f as incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) by A13, A15, 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 A13, A14, Def5; :: thesis: verum

end;

suppose A16: 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 Th24;
reconsider f = f as incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) by A13, 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 A13, A16; :: thesis: verum

end;

end;

end;

end;