let R be Ring; :: thesis: for S being RingExtension of R
for a being Element of R
for b being Element of S st b = a holds
for i being Integer holds i '*' a = i '*' b
let S be RingExtension of R; :: thesis: for a being Element of R
for b being Element of S st b = a holds
for i being Integer holds i '*' a = i '*' b
let a be Element of R; :: thesis: for b being Element of S st b = a holds
for i being Integer holds i '*' a = i '*' b
let b be Element of S; :: thesis: ( b = a implies for i being Integer holds i '*' a = i '*' b )
assume AS: b = a ; :: thesis: for i being Integer holds i '*' a = i '*' b
let i be Integer; :: thesis: i '*' a = i '*' b
K: R is Subring of S by FIELD_4:def 1;
defpred S₁[ Integer] means for k being Integer st k = $1 holds
k '*' a = k '*' b;

now :: thesis: for k being Integer st k = 0 holds
k '*' a = k '*' b

let k be Integer; :: thesis: ( k = 0 implies k '*' a = k '*' b )
assume A1: k = 0 ; :: thesis: k '*' a = k '*' b
hence k '*' a = 0. R by RING_3:59
.= 0. S by K, C0SP1:def 3
.= k '*' b by A1, RING_3:59 ;
:: thesis: verum

end;

then A2: S₁[ 0 ] ;
A6: 1 '*' a = b by AS, RING_3:60
.= 1 '*' b by RING_3:60 ;
then A7: - (1 '*' a) = - (1 '*' b) by K, FIELD_6:17;
A3: for u being Integer st S₁[u] holds
( S₁[u - 1] & S₁[u + 1] )

proof

let u be Integer; :: thesis: ( S₁[u] implies ( S₁[u - 1] & S₁[u + 1] ) )
assume S₁[u] ; :: thesis: ( S₁[u - 1] & S₁[u + 1] )
then A4: u '*' a = u '*' b ;

now :: thesis: for k being Integer st k = u - 1 holds
k '*' a = k '*' b

let k be Integer; :: thesis: ( k = u - 1 implies k '*' a = k '*' b )
assume A5: k = u - 1 ; :: thesis: k '*' a = k '*' b
hence k '*' a = (u '*' a) - (1 '*' a) by RING_3:64
.= (u '*' b) - (1 '*' b) by A4, A7, K, FIELD_6:15
.= k '*' b by A5, RING_3:64 ;
:: thesis: verum

end;

hence S₁[u - 1] ; :: thesis: S₁[u + 1]

now :: thesis: for k being Integer st k = u + 1 holds
k '*' a = k '*' b

let k be Integer; :: thesis: ( k = u + 1 implies k '*' a = k '*' b )
assume A5: k = u + 1 ; :: thesis: k '*' a = k '*' b
hence k '*' a = (u '*' a) + (1 '*' a) by RING_3:62
.= (u '*' b) + (1 '*' b) by A4, A6, K, FIELD_6:15
.= k '*' b by A5, RING_3:62 ;
:: thesis: verum

end;

hence S₁[u + 1] ; :: thesis: verum

end;

for i being Integer holds S₁[i] from INT_1:sch 4(A2, A3);
hence i '*' a = i '*' b ; :: thesis: verum