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:9;
k - 1 <= (dim p) - 0 by A2, XREAL_1:13;
hence (k - 1) -polytopes p <> {} by A4, Th23; :: thesis: verum
end;
( dom (eta (p,k)) = [:((k - 1) -polytopes p),(k -polytopes p):] & k -polytopes p <> {} ) by A1, A2, Th23, FUNCT_2:92;
then [x,y] in dom (eta (p,k)) by A3, ZFMISC_1:87;
then (eta (p,k)) . [x,y] in rng (eta (p,k)) by FUNCT_1:3;
hence (eta (p,k)) . (x,y) is Element of Z_2 by BSPACE:3, BSPACE:5, BSPACE:6; :: thesis: verum