let F be Ring; :: thesis: for S being RingExtension of F
for a being Element of F
for b being Element of S st a = b holds
a | F = b | S
let E be RingExtension of F; :: thesis: for a being Element of F
for b being Element of E st a = b holds
a | F = b | E
let a be Element of F; :: thesis: for b being Element of E st a = b holds
a | F = b | E
let b be Element of E; :: thesis: ( a = b implies a | F = b | E )
assume AS: a = b ; :: thesis: a | F = b | E
set ap = a | F;
set bp = b | E;
X: F is Subring of E by FIELD_4:def 1;

now :: thesis: for n being Element of NAT holds (a | F) . n = (b | E) . n

let n be Element of NAT ; :: thesis: (a | F) . b₁ = (b | E) . b₁

per cases ( n = 0 or n <> 0 ) ;

suppose A: n = 0 ; :: thesis: (a | F) . b₁ = (b | E) . b₁

hence (a | F) . n = b by AS, Th28
.= (b | E) . n by A, Th28 ;
:: thesis: verum

end;

suppose A: n <> 0 ; :: thesis: (a | F) . b₁ = (b | E) . b₁

hence (a | F) . n = 0. F by Th28
.= 0. E by X, C0SP1:def 3
.= (b | E) . n by A, Th28 ;
:: thesis: verum

end;

end;

end;

hence a | F = b | E ; :: thesis: verum