let R be Field; :: thesis: for F being Subfield of R
for x being non zero Element of R
for x1 being Element of F st x = x1 holds
x " = x1 "
let S be Subfield of R; :: thesis: for x being non zero Element of R
for x1 being Element of S st x = x1 holds
x " = x1 "
let x be non zero Element of R; :: thesis: for x1 being Element of S st x = x1 holds
x " = x1 "
let x1 be Element of S; :: thesis: ( x = x1 implies x " = x1 " )
set C = the carrier of R;
set C1 = the carrier of S;
set a = x1 " ;
assume A1: x = x1 ; :: thesis: x " = x1 "
A2: x <> 0. R ;
then A3: x1 <> 0. S by A1, EC_PF_1:def 1;
the carrier of S c= the carrier of R by EC_PF_1:def 1;
then reconsider g = x1 " as Element of R ;
R is FieldExtension of S by FIELD_4:7;
then S is Subring of R by FIELD_4:def 1;
then g * x = (x1 ") * x1 by A1, Th18
.= 1. S by A3, VECTSP_1:def 10
.= 1. R by EC_PF_1:def 1 ;
hence x " = x1 " by A2, VECTSP_1:def 10; :: thesis: verum