theorem ZMATRLIN43: :: ZMODLAT2:47

for i being Nat
for j being Element of F_Real
for k being Element of F_Rat st j = k holds
((power F_Real) . ((- (1_ F_Real)),i)) * j = ((power F_Rat) . ((- (1_ F_Rat)),i)) * k