theorem LmSign1D: :: ZMATRLIN:43

for i being Nat
for j being Element of F_Real st j in INT holds
((power F_Real) . ((- (1_ F_Real)),i)) * j in INT