let F be Ring; :: thesis: for S being RingExtension of F
for a being Element of F
for b being Element of S
for n being Element of NAT st a = b holds
n * a = n * b
let E be RingExtension of F; :: thesis: for a being Element of F
for b being Element of E
for n being Element of NAT st a = b holds
n * a = n * b
let a be Element of F; :: thesis: for b being Element of E
for n being Element of NAT st a = b holds
n * a = n * b
let b be Element of E; :: thesis: for n being Element of NAT st a = b holds
n * a = n * b
let n be Element of NAT ; :: thesis: ( a = b implies n * a = n * b )
assume AS: a = b ; :: thesis: n * a = n * b
defpred S₁[ Nat] means $1 * a = $1 * b;
H: F is Subring of E by FIELD_4:def 1;
0 * a = 0. F by BINOM:12
.= 0. E by H, C0SP1:def 3
.= 0 * b by BINOM:12 ;
then A: S₁[ 0 ] ;

B: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume C: S₁[k] ; :: thesis: S₁[k + 1]
(k + 1) * a = (k * a) + (1 * a) by BINOM:15
.= (k * a) + a by BINOM:13
.= (k * b) + b by H, C, AS, FIELD_6:15
.= (k * b) + (1 * b) by BINOM:13
.= (k + 1) * b by BINOM:15 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A, B);
hence n * a = n * b ; :: thesis: verum