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 S1[ 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: S1[ 0 ] ;
A3: for i being Integer st S1[i] holds
( S1[i - 1] & S1[i + 1] )
proof
let i be Integer; :: thesis: ( S1[i] implies ( S1[i - 1] & S1[i + 1] ) )
assume A4: S1[i] ; :: thesis: ( S1[i - 1] & S1[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 S1[i - 1] ; :: thesis: S1[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 S1[i + 1] ; :: thesis: verum
end;
for i being Integer holds S1[i] from INT_1:sch 4(A2, A3);
 hence f . (i '*' a) = i '*' (f . a) ; :: thesis: verum