let n be Nat; for K being Field
for V1 being VectSp of K
for L being Scalar of K holds (L * (id V1)) |^ n = ((power K) . (L,n)) * (id V1)
let K be Field; for V1 being VectSp of K
for L being Scalar of K holds (L * (id V1)) |^ n = ((power K) . (L,n)) * (id V1)
let V1 be VectSp of K; for L being Scalar of K holds (L * (id V1)) |^ n = ((power K) . (L,n)) * (id V1)
let L be Scalar of K; (L * (id V1)) |^ n = ((power K) . (L,n)) * (id V1)
defpred S1[ Nat] means (L * (id V1)) |^ $1 = ((power K) . (L,$1)) * (id V1);
A1:
( dom (id V1) = [#] V1 & dom ((1_ K) * (id V1)) = [#] V1 )
by FUNCT_2:def 1;
A3:
for n being Nat st S1[n] holds
S1[n + 1]
( (L * (id V1)) |^ 0 = id V1 & (power K) . (L,0) = 1_ K )
by Th18, GROUP_1:def 7;
then A5:
S1[ 0 ]
by A1, A2, FUNCT_1:2;
for n being Nat holds S1[n]
from NAT_1:sch 2(A5, A3);
hence
(L * (id V1)) |^ n = ((power K) . (L,n)) * (id V1)
; verum