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 & y = y1 holds
x - y = x1 - y1
let K1 be Subfield of K; :: thesis: for x, y being Element of K
for x1, y1 being Element of K1 st x = x1 & y = y1 holds
x - y = x1 - y1
let x, y be Element of K; :: thesis: for x1, y1 being Element of K1 st x = x1 & y = y1 holds
x - y = x1 - y1
let x1, y1 be Element of K1; :: thesis: ( x = x1 & y = y1 implies x - y = x1 - y1 )
set C1 = the carrier of K1;
assume A1: ( x = x1 & y = y1 ) ; :: thesis: x - y = x1 - y1
then A2: - y = - y1 by Th19;
the addF of K1 = the addF of K || the carrier of K1 by EC_PF_1:def 1;
hence x - y = x1 - y1 by A1, A2, FUNCT_1:49, ZFMISC_1:87; :: thesis: verum