let n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: for L being Scalar of K holds (L * (id V1)) |^ n = ((power K) . (L,n)) * (id V1)
let L be Scalar of K; :: thesis: (L * (id V1)) |^ n = ((power K) . (L,n)) * (id V1)
defpred S₁[ 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;

A2: now :: thesis: for x being object st x in [#] V1 holds
(id V1) . x = ((1_ K) * (id V1)) . x

let x be object ; :: thesis: ( x in [#] V1 implies (id V1) . x = ((1_ K) * (id V1)) . x )
assume x in [#] V1 ; :: thesis: (id V1) . x = ((1_ K) * (id V1)) . x
then reconsider v = x as Vector of V1 ;
( (id V1) . x = v & (1_ K) * v = v ) ;
hence (id V1) . x = ((1_ K) * (id V1)) . x by MATRLIN:def 4; :: thesis: verum

end;

A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
thus (L * (id V1)) |^ (n + 1) = ((L * (id V1)) |^ 1) * (((power K) . (L,n)) * (id V1)) by A4, Th20
.= (L * (id V1)) * (((power K) . (L,n)) * (id V1)) by Th19
.= ((power K) . (L,n)) * ((L * (id V1)) * (id V1)) by Lm5
.= ((power K) . (L,n)) * (L * ((id V1) * (id V1))) by Lm4
.= ((power K) . (L,n)) * (L * (id V1)) by SYSREL:12
.= (((power K) . (L,n)) * L) * (id V1) by Lm3
.= ((power K) . (L,(n + 1))) * (id V1) by GROUP_1:def 7 ; :: thesis: verum

end;

( (L * (id V1)) |^ 0 = id V1 & (power K) . (L,0) = 1_ K ) by Th18, GROUP_1:def 7;
then A5: S₁[ 0 ] by A1, A2, FUNCT_1:2;
for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A3);
hence (L * (id V1)) |^ n = ((power K) . (L,n)) * (id V1) ; :: thesis: verum