let K be Field; :: thesis: for K1 being Subfield of K
for x being Element of K
for x1 being Element of K1 st x = x1 holds
- x = - x1
let K1 be Subfield of K; :: thesis: for x being Element of K
for x1 being Element of K1 st x = x1 holds
- x = - x1
let x be Element of K; :: thesis: for x1 being Element of K1 st x = x1 holds
- x = - x1
let x1 be Element of K1; :: thesis: ( x = x1 implies - x = - x1 )
set C = the carrier of K;
set C1 = the carrier of K1;
set hpd = - x1;
assume A1: x = x1 ; :: thesis: - x = - x1
the carrier of K1 c= the carrier of K by EC_PF_1:def 1;
then reconsider g = - x1 as Element of K ;
x + g = x1 + (- x1) by A1, Th17
.= 0. K1 by VECTSP_1:19
.= 0. K by EC_PF_1:def 1 ;
hence - x = - x1 by VECTSP_1:16; :: thesis: verum