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: S₁[ 0 ]

proof

A2: ( (L * (id V1)) |^ 0 = id V1 & (power K) . L,0 = 1_ K ) by Th18, GROUP_1:def 8;
A3: ( dom (id V1) = [#] V1 & dom ((1_ K) * (id V1)) = [#] V1 ) by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in [#] V1 implies (id V1) . x = ((1_ K) * (id V1)) . x )
assume A4: x in [#] V1 ; :: thesis: (id V1) . x = ((1_ K) * (id V1)) . x
reconsider v = x as Vector of V1 by A4;
( (id V1) . x = v & (1_ K) * v = v ) by FUNCT_1:35, VECTSP_1:def 26;
hence (id V1) . x = ((1_ K) * (id V1)) . x by MATRLIN:def 6; :: thesis: verum

end;

hence S₁[ 0 ] by A2, A3, FUNCT_1:9; :: thesis: verum

end;

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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A6: S₁[n] ; :: thesis: S₁[n + 1]
A7: n in NAT by ORDINAL1:def 13;
thus (L * (id V1)) |^ (n + 1) = ((L * (id V1)) |^ 1) * (((power K) . L,n) * (id V1)) by A6, 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:29
.= (((power K) . L,n) * L) * (id V1) by Lm3
.= ((power K) . L,(n + 1)) * (id V1) by A7, GROUP_1:def 8 ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A5);
hence (L * (id V1)) |^ n = ((power K) . L,n) * (id V1) ; :: thesis: verum