set n = eta p,k;
A2: dom (eta p,k) = [:((k - 1) -polytopes p),(k -polytopes p):] by FUNCT_2:169;
A3: (k - 1) -polytopes p <> {}

proof

set m = k - 1;
0 - 1 = - 1 ;
then A4: - 1 <= k - 1 by A1, XREAL_1:11;
k - 1 <= (dim p) - 0 by A1, XREAL_1:15;
hence (k - 1) -polytopes p <> {} by A4, Th26; :: thesis: verum

end;

k -polytopes p <> {} by A1, Th26;
then A5: [x,y] in dom (eta p,k) by A2, A3, ZFMISC_1:106;
A6: rng (eta p,k) c= {(0. Z_2 ),(1. Z_2 )} by FUNCT_2:169;
(eta p,k) . [x,y] in rng (eta p,k) by A5, FUNCT_1:12;
hence (eta p,k) . x,y is Element of Z_2 by A6, BSPACE:3, BSPACE:5, BSPACE:6; :: thesis: verum