let i be Nat; :: thesis: (power F_Real) . ((- (1_ F_Real)),i) in F_Rat
((power F_Real) . ((- (1_ F_Real)),i)) * (1. F_Real) = ((power F_Rat) . ((- (1_ F_Rat)),i)) * (1. F_Rat) by ZMATRLIN43;
hence (power F_Real) . ((- (1_ F_Real)),i) in F_Rat ; :: thesis: verum