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