let i, j be Nat; :: thesis: for K being Field
for a, aj being Element of K
for R being Element of () 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 () 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 () st j in Seg i & aj = R . j holds
(a * R) . j = a * aj

let R be Element of (); :: 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 -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 = () . (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 ;
hence (a * R) . j = a * aj by ; :: thesis: verum