theorem LmSign1D: :: ZMODLAT2:49

for i being Nat holds (power F_Real) . ((- (1_ F_Real)),i) in F_Rat