let K be Field; :: thesis: for K1 being Subfield of K
for x, y being Element of K
for x1, y1 being Element of K1 st x = x1 & x <> 0. K holds
x " = x1 "
let K1 be Subfield of K; :: thesis: for x, y being Element of K
for x1, y1 being Element of K1 st x = x1 & x <> 0. K holds
x " = x1 "
let x, y be Element of K; :: thesis: for x1, y1 being Element of K1 st x = x1 & x <> 0. K holds
x " = x1 "
let x1, y1 be Element of K1; :: thesis: ( x = x1 & x <> 0. K implies x " = x1 " )
set C = the carrier of K;
set C1 = the carrier of K1;
set hpd = x1 " ;
assume A1: ( x = x1 & x <> 0. K ) ; :: thesis: x " = x1 "
then A2: x1 <> 0. K1 by EC_PF_1:def 1;
the carrier of K1 c= the carrier of K by EC_PF_1:def 1;
then reconsider g = x1 " as Element of K ;
A3: x * g = x1 * (x1 ") by A1, Th18
.= 1. K1 by A2, VECTSP_1:def 10 ;
x * g = 1. K by A3, EC_PF_1:def 1;
hence x " = x1 " by A1, VECTSP_1:def 10; :: thesis: verum