let K be Field; 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; 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; for x1, y1 being Element of K1 st x = x1 & y = y1 holds
x - y = x1 - y1
let x1, y1 be Element of K1; ( x = x1 & y = y1 implies x - y = x1 - y1 )
set C1 = the carrier of K1;
assume A1:
( x = x1 & y = y1 )
; 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; verum