for n being non zero Nat
for i being Nat holds Proj (i,n) = ((proj (1,1)) ") * (proj (i,n))