theorem LmSign1A: :: ZMODLAT2:54
for n being Nat
for M being Matrix of n,F_Real
for H being Matrix of n,F_Rat st M = H holds
Det M = Det H