let n be Nat; :: thesis: for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K st n >= 1 holds
ex h being linear-transformation of V1,V1 st
( (f + (L * (id V1))) |^ n = (f * h) + ((L * (id V1)) |^ n) & ( for i being Nat holds (f |^ i) * h = h * (f |^ i) ) )
let K be Field; :: thesis: for V1 being VectSp of K
for f being linear-transformation of V1,V1
for L being Scalar of K st n >= 1 holds
ex h being linear-transformation of V1,V1 st
( (f + (L * (id V1))) |^ n = (f * h) + ((L * (id V1)) |^ n) & ( for i being Nat holds (f |^ i) * h = h * (f |^ i) ) )
let V1 be VectSp of K; :: thesis: for f being linear-transformation of V1,V1
for L being Scalar of K st n >= 1 holds
ex h being linear-transformation of V1,V1 st
( (f + (L * (id V1))) |^ n = (f * h) + ((L * (id V1)) |^ n) & ( for i being Nat holds (f |^ i) * h = h * (f |^ i) ) )
let f be linear-transformation of V1,V1; :: thesis: for L being Scalar of K st n >= 1 holds
ex h being linear-transformation of V1,V1 st
( (f + (L * (id V1))) |^ n = (f * h) + ((L * (id V1)) |^ n) & ( for i being Nat holds (f |^ i) * h = h * (f |^ i) ) )
let L be Scalar of K; :: thesis: ( n >= 1 implies ex h being linear-transformation of V1,V1 st
( (f + (L * (id V1))) |^ n = (f * h) + ((L * (id V1)) |^ n) & ( for i being Nat holds (f |^ i) * h = h * (f |^ i) ) ) )
set g = L * (id V1);
defpred S₁[ Nat] means ex h being linear-transformation of V1,V1 st
( (f + (L * (id V1))) |^ $1 = (f * h) + ((L * (id V1)) |^ $1) & ( for i being Nat holds (f |^ i) * h = h * (f |^ i) ) );
A1: for n being Nat st 1 <= n & S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( 1 <= n & S₁[n] implies S₁[n + 1] )
assume 1 <= n ; :: thesis: ( not S₁[n] or S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then consider h being linear-transformation of V1,V1 such that
A2: (f + (L * (id V1))) |^ n = (f * h) + ((L * (id V1)) |^ n) and
A3: for i being Nat holds (f |^ i) * h = h * (f |^ i) ;
take H = ((f * h) + ((L * (id V1)) |^ n)) + (L * h); :: thesis: ( (f + (L * (id V1))) |^ (n + 1) = (f * H) + ((L * (id V1)) |^ (n + 1)) & ( for i being Nat holds (f |^ i) * H = H * (f |^ i) ) )
A4: rng (f * h) c= [#] V1 by RELAT_1:def 19;
thus (f + (L * (id V1))) |^ (n + 1) = ((f + (L * (id V1))) |^ 1) * ((f + (L * (id V1))) |^ n) by Th20
.= (f + (L * (id V1))) * ((f * h) + ((L * (id V1)) |^ n)) by A2, Th19
.= (f * ((f * h) + ((L * (id V1)) |^ n))) + ((L * (id V1)) * ((f * h) + ((L * (id V1)) |^ n))) by Lm6
.= (f * ((f * h) + ((L * (id V1)) |^ n))) + (((L * (id V1)) * (f * h)) + ((L * (id V1)) * ((L * (id V1)) |^ n))) by Lm7
.= ((f * ((f * h) + ((L * (id V1)) |^ n))) + ((L * (id V1)) * (f * h))) + ((L * (id V1)) * ((L * (id V1)) |^ n)) by Lm8
.= ((f * ((f * h) + ((L * (id V1)) |^ n))) + (L * ((id V1) * (f * h)))) + ((L * (id V1)) * ((L * (id V1)) |^ n)) by Lm4
.= ((f * ((f * h) + ((L * (id V1)) |^ n))) + (L * (f * h))) + ((L * (id V1)) * ((L * (id V1)) |^ n)) by A4, RELAT_1:53
.= ((f * ((f * h) + ((L * (id V1)) |^ n))) + (f * (L * h))) + ((L * (id V1)) * ((L * (id V1)) |^ n)) by Lm5
.= (f * H) + ((L * (id V1)) * ((L * (id V1)) |^ n)) by Lm7
.= (f * H) + (((L * (id V1)) |^ 1) * ((L * (id V1)) |^ n)) by Th19
.= (f * H) + ((L * (id V1)) |^ (n + 1)) by Th20 ; :: thesis: for i being Nat holds (f |^ i) * H = H * (f |^ i)
let i be Nat; :: thesis: (f |^ i) * H = H * (f |^ i)
A5: (f |^ i) * (f * h) = ((f |^ i) * f) * h by RELAT_1:36
.= ((f |^ i) * (f |^ 1)) * h by Th19
.= (f |^ (i + 1)) * h by Th20
.= h * (f |^ (i + 1)) by A3
.= h * ((f |^ 1) * (f |^ i)) by Th20
.= (h * (f |^ 1)) * (f |^ i) by RELAT_1:36
.= ((f |^ 1) * h) * (f |^ i) by A3
.= (f * h) * (f |^ i) by Th19 ;
A6: (f |^ i) * ((L * (id V1)) |^ n) = (f |^ i) * (((power K) . (L,n)) * (id V1)) by Lm9
.= ((power K) . (L,n)) * ((f |^ i) * (id V1)) by Lm5
.= ((power K) . (L,n)) * ((f |^ i) * (f |^ 0)) by Th18
.= ((power K) . (L,n)) * (f |^ (i + 0)) by Th20
.= ((power K) . (L,n)) * ((f |^ 0) * (f |^ i)) by Th20
.= ((power K) . (L,n)) * ((id V1) * (f |^ i)) by Th18
.= (((power K) . (L,n)) * (id V1)) * (f |^ i) by Lm4
.= ((L * (id V1)) |^ n) * (f |^ i) by Lm9 ;
(f |^ i) * (L * h) = L * ((f |^ i) * h) by Lm5
.= L * (h * (f |^ i)) by A3
.= (L * h) * (f |^ i) by Lm4 ;
hence (f |^ i) * H = ((f |^ i) * ((f * h) + ((L * (id V1)) |^ n))) + ((L * h) * (f |^ i)) by Lm7
.= (((f * h) * (f |^ i)) + (((L * (id V1)) |^ n) * (f |^ i))) + ((L * h) * (f |^ i)) by A5, A6, Lm7
.= (((f * h) + ((L * (id V1)) |^ n)) * (f |^ i)) + ((L * h) * (f |^ i)) by Lm6
.= H * (f |^ i) by Lm6 ;
:: thesis: verum

end;

A7: S₁[1]

proof

take h = id V1; :: thesis: ( (f + (L * (id V1))) |^ 1 = (f * h) + ((L * (id V1)) |^ 1) & ( for i being Nat holds (f |^ i) * h = h * (f |^ i) ) )
thus (f + (L * (id V1))) |^ 1 = f + (L * (id V1)) by Th19
.= (f |^ (1 + 0)) + (L * (id V1)) by Th19
.= ((f |^ 1) * (f |^ 0)) + (L * (id V1)) by Th20
.= ((f |^ 1) * h) + (L * (id V1)) by Th18
.= (f * h) + (L * (id V1)) by Th19
.= (f * h) + ((L * (id V1)) |^ 1) by Th19 ; :: thesis: for i being Nat holds (f |^ i) * h = h * (f |^ i)
let i be Nat; :: thesis: (f |^ i) * h = h * (f |^ i)
thus (f |^ i) * h = (f |^ i) * (f |^ 0) by Th18
.= f |^ (i + 0) by Th20
.= (f |^ 0) * (f |^ i) by Th20
.= h * (f |^ i) by Th18 ; :: thesis: verum

end;

for n being Nat st 1 <= n holds
S₁[n] from NAT_1:sch 8(A7, A1);
hence ( n >= 1 implies ex h being linear-transformation of V1,V1 st
( (f + (L * (id V1))) |^ n = (f * h) + ((L * (id V1)) |^ n) & ( for i being Nat holds (f |^ i) * h = h * (f |^ i) ) ) ) ; :: thesis: verum