let i, j be Nat; :: thesis: for K being Field

for a, aj being Element of K

for R being Element of (i -VectSp_over K) st j in Seg i & aj = R . j holds

(a * R) . j = a * aj

let K be Field; :: thesis: for a, aj being Element of K

for R being Element of (i -VectSp_over K) st j in Seg i & aj = R . j holds

(a * R) . j = a * aj

let a, aj be Element of K; :: thesis: for R being Element of (i -VectSp_over K) st j in Seg i & aj = R . j holds

(a * R) . j = a * aj

let R be Element of (i -VectSp_over K); :: thesis: ( j in Seg i & aj = R . j implies (a * R) . j = a * aj )

assume AS: ( j in Seg i & aj = R . j ) ; :: thesis: (a * R) . j = a * aj

P0: the carrier of (i -VectSp_over K) = i -tuples_on the carrier of K by MATRIX13:102;

reconsider R0 = R as Element of i -tuples_on the carrier of K by MATRIX13:102;

P3: a * R = (i -Mult_over K) . (a,R) by PRVECT_1:def 5

.= the multF of K [;] (a,R0) by PRVECT_1:def 4 ;

a * R in i -tuples_on the carrier of K by P0;

then consider s being Element of the carrier of K * such that

P4: ( a * R = s & len s = i ) ;

dom ( the multF of K [;] (a,R0)) = Seg i by P3, P4, FINSEQ_1:def 3;

hence (a * R) . j = a * aj by P3, AS, FUNCOP_1:32; :: thesis: verum

for a, aj being Element of K

for R being Element of (i -VectSp_over K) st j in Seg i & aj = R . j holds

(a * R) . j = a * aj

let K be Field; :: thesis: for a, aj being Element of K

for R being Element of (i -VectSp_over K) st j in Seg i & aj = R . j holds

(a * R) . j = a * aj

let a, aj be Element of K; :: thesis: for R being Element of (i -VectSp_over K) st j in Seg i & aj = R . j holds

(a * R) . j = a * aj

let R be Element of (i -VectSp_over K); :: thesis: ( j in Seg i & aj = R . j implies (a * R) . j = a * aj )

assume AS: ( j in Seg i & aj = R . j ) ; :: thesis: (a * R) . j = a * aj

P0: the carrier of (i -VectSp_over K) = i -tuples_on the carrier of K by MATRIX13:102;

reconsider R0 = R as Element of i -tuples_on the carrier of K by MATRIX13:102;

P3: a * R = (i -Mult_over K) . (a,R) by PRVECT_1:def 5

.= the multF of K [;] (a,R0) by PRVECT_1:def 4 ;

a * R in i -tuples_on the carrier of K by P0;

then consider s being Element of the carrier of K * such that

P4: ( a * R = s & len s = i ) ;

dom ( the multF of K [;] (a,R0)) = Seg i by P3, P4, FINSEQ_1:def 3;

hence (a * R) . j = a * aj by P3, AS, FUNCOP_1:32; :: thesis: verum