(1. F_Complex) + (In ((- (1. F_Rat)),F_Complex)) = (In ((1. F_Rat),F_Complex)) + (In ((- (1. F_Rat)),F_Complex)) by Lm5, Th3
.= In ((0. F_Rat),F_Complex)
.= 0. F_Complex by Lm5, Th3 ;
hence In ((- (1. F_Rat)),F_Complex) = - (1. F_Complex) by RLVECT_1:def 10; :: thesis: verum