let R be Ring; :: thesis: for S being R -homomorphic Ring
for f being Homomorphism of R,S
for a being Element of R
for i being Integer holds f . (i '*' a) = i '*' (f . a)
let S be R -homomorphic Ring; :: thesis: for f being Homomorphism of R,S
for a being Element of R
for i being Integer holds f . (i '*' a) = i '*' (f . a)
let f be Homomorphism of R,S; :: thesis: for a being Element of R
for i being Integer holds f . (i '*' a) = i '*' (f . a)
let a be Element of R; :: thesis: for i being Integer holds f . (i '*' a) = i '*' (f . a)
let i be Integer; :: thesis: f . (i '*' a) = i '*' (f . a)
defpred S₁[ Integer] means for j being Integer st j = $1 holds
f . (j '*' a) = j '*' (f . a);

now :: thesis: for j being Integer st j = 0 holds
f . (j '*' a) = j '*' (f . a)

let j be Integer; :: thesis: ( j = 0 implies f . (j '*' a) = j '*' (f . a) )
assume A1: j = 0 ; :: thesis: f . (j '*' a) = j '*' (f . a)
hence f . (j '*' a) = f . (0. R) by Th58
.= 0. S by RING_2:6
.= j '*' (f . a) by A1, Th58 ;
:: thesis: verum

end;

then A2: S₁[ 0 ] ;
A3: for i being Integer st S₁[i] holds
( S₁[i - 1] & S₁[i + 1] )

proof

let i be Integer; :: thesis: ( S₁[i] implies ( S₁[i - 1] & S₁[i + 1] ) )
assume A4: S₁[i] ; :: thesis: ( S₁[i - 1] & S₁[i + 1] )

now :: thesis: for k being Integer st k = i - 1 holds
f . (k '*' a) = k '*' (f . a)

let k be Integer; :: thesis: ( k = i - 1 implies f . (k '*' a) = k '*' (f . a) )
assume k = i - 1 ; :: thesis: f . (k '*' a) = k '*' (f . a)
then A5: f . ((k + 1) '*' a) = (k + 1) '*' (f . a) by A4
.= (k '*' (f . a)) + (1 '*' (f . a)) by Th61
.= (k '*' (f . a)) + (f . a) by Th59 ;
f . ((k + 1) '*' a) = f . ((k '*' a) + (1 '*' a)) by Th61
.= f . ((k '*' a) + a) by Th59
.= (f . (k '*' a)) + (f . a) by VECTSP_1:def 20 ;
hence f . (k '*' a) = k '*' (f . a) by A5, RLVECT_1:8; :: thesis: verum

end;

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

now :: thesis: for k being Integer st k = i + 1 holds
f . (k '*' a) = k '*' (f . a)

let k be Integer; :: thesis: ( k = i + 1 implies f . (k '*' a) = k '*' (f . a) )
assume k = i + 1 ; :: thesis: f . (k '*' a) = k '*' (f . a)
then A6: f . ((k - 1) '*' a) = (k - 1) '*' (f . a) by A4
.= (k '*' (f . a)) + ((- (1. INT.Ring)) '*' (f . a)) by Th61
.= (k '*' (f . a)) - (f . a) by Th60 ;
f . ((k - 1) '*' a) = f . ((k '*' a) + ((- (1. INT.Ring)) '*' a)) by Th61
.= f . ((k '*' a) - a) by Th60
.= (f . (k '*' a)) - (f . a) by RING_2:8 ;
hence f . (k '*' a) = k '*' (f . a) by A6, RLVECT_1:8; :: thesis: verum

end;

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

end;

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