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

let A, B be Element of (); :: 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 (), the addF of (), the ZeroF of () #) = 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 -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 ;
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 ;
hence (A + B) . j = aj + bj by ; :: thesis: verum