let i, j be Nat; :: thesis: for K being Field
for aj, bj being Element of K
for A, B being Element of (i -VectSp_over K) st j in Seg i & aj = A . j & bj = B . j holds
(A + B) . j = aj + bj
let K be Field; :: thesis: for aj, bj being Element of K
for A, B being Element of (i -VectSp_over K) st j in Seg i & aj = A . j & bj = B . j holds
(A + B) . j = aj + bj
let aj, bj be Element of K; :: thesis: for A, B being Element of (i -VectSp_over K) st j in Seg i & aj = A . j & bj = B . j holds
(A + B) . j = aj + bj
let A, B be Element of (i -VectSp_over K); :: thesis: ( j in Seg i & aj = A . j & bj = B . j implies (A + B) . j = aj + bj )
assume AS: ( j in Seg i & aj = A . j & bj = B . j ) ; :: thesis: (A + B) . j = aj + bj
P1: addLoopStr(# the carrier of (i -VectSp_over K), the addF of (i -VectSp_over K), the ZeroF of (i -VectSp_over K) #) = i -Group_over K by PRVECT_1:def 5;
P2: i -Group_over K = addLoopStr(# (i -tuples_on the carrier of K),(product ( the addF of K,i)),(i |-> (0. K)) #) by PRVECT_1:def 3;
P0: the carrier of (i -VectSp_over K) = i -tuples_on the carrier of K by MATRIX13:102;
reconsider A0 = A, B0 = B as Element of i -tuples_on the carrier of K by MATRIX13:102;
P3: A + B = the addF of K .: (A0,B0) by P1, P2, PRVECT_1:def 1;
A + B in i -tuples_on the carrier of K by P0;
then consider s being Element of the carrier of K * such that
P4: ( A + B = s & len s = i ) ;
dom ( the addF of K .: (A0,B0)) = Seg i by P3, P4, FINSEQ_1:def 3;
hence (A + B) . j = aj + bj by P3, AS, FUNCOP_1:22; :: thesis: verum