set n = eta p,k;
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 A2, XREAL_1:15;
hence (k - 1) -polytopes p <> {} by A4, Th26; :: thesis: verum

end;

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