let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K

for a being Element of V1

for F being FinSequence of K

for G being FinSequence of V1 st len F = len G & ( for k being Nat st k in dom F holds

G . k = (F /. k) * a ) holds

Sum G = (Sum F) * a

let V1 be finite-dimensional VectSp of K; :: thesis: for a being Element of V1

for F being FinSequence of K

for G being FinSequence of V1 st len F = len G & ( for k being Nat st k in dom F holds

G . k = (F /. k) * a ) holds

Sum G = (Sum F) * a

let a be Element of V1; :: thesis: for F being FinSequence of K

for G being FinSequence of V1 st len F = len G & ( for k being Nat st k in dom F holds

G . k = (F /. k) * a ) holds

Sum G = (Sum F) * a

let F be FinSequence of K; :: thesis: for G being FinSequence of V1 st len F = len G & ( for k being Nat st k in dom F holds

G . k = (F /. k) * a ) holds

Sum G = (Sum F) * a

let G be FinSequence of V1; :: thesis: ( len F = len G & ( for k being Nat st k in dom F holds

G . k = (F /. k) * a ) implies Sum G = (Sum F) * a )

assume that

A1: len F = len G and

A2: for k being Nat st k in dom F holds

G . k = (F /. k) * a ; :: thesis: Sum G = (Sum F) * a

for a being Element of V1

for F being FinSequence of K

for G being FinSequence of V1 st len F = len G & ( for k being Nat st k in dom F holds

G . k = (F /. k) * a ) holds

Sum G = (Sum F) * a

let V1 be finite-dimensional VectSp of K; :: thesis: for a being Element of V1

for F being FinSequence of K

for G being FinSequence of V1 st len F = len G & ( for k being Nat st k in dom F holds

G . k = (F /. k) * a ) holds

Sum G = (Sum F) * a

let a be Element of V1; :: thesis: for F being FinSequence of K

for G being FinSequence of V1 st len F = len G & ( for k being Nat st k in dom F holds

G . k = (F /. k) * a ) holds

Sum G = (Sum F) * a

let F be FinSequence of K; :: thesis: for G being FinSequence of V1 st len F = len G & ( for k being Nat st k in dom F holds

G . k = (F /. k) * a ) holds

Sum G = (Sum F) * a

let G be FinSequence of V1; :: thesis: ( len F = len G & ( for k being Nat st k in dom F holds

G . k = (F /. k) * a ) implies Sum G = (Sum F) * a )

assume that

A1: len F = len G and

A2: for k being Nat st k in dom F holds

G . k = (F /. k) * a ; :: thesis: Sum G = (Sum F) * a

now :: thesis: for k being Nat

for v being Element of K st k in dom G & v = F . k holds

G . k = v * a

hence
Sum G = (Sum F) * a
by A1, Th9; :: thesis: verumfor v being Element of K st k in dom G & v = F . k holds

G . k = v * a

let k be Nat; :: thesis: for v being Element of K st k in dom G & v = F . k holds

G . k = v * a

let v be Element of K; :: thesis: ( k in dom G & v = F . k implies G . k = v * a )

assume that

A3: k in dom G and

A4: v = F . k ; :: thesis: G . k = v * a

A5: k in dom F by A1, A3, FINSEQ_3:29;

then v = F /. k by A4, PARTFUN1:def 6;

hence G . k = v * a by A2, A5; :: thesis: verum

end;G . k = v * a

let v be Element of K; :: thesis: ( k in dom G & v = F . k implies G . k = v * a )

assume that

A3: k in dom G and

A4: v = F . k ; :: thesis: G . k = v * a

A5: k in dom F by A1, A3, FINSEQ_3:29;

then v = F /. k by A4, PARTFUN1:def 6;

hence G . k = v * a by A2, A5; :: thesis: verum