let i, j be Nat; 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; 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; 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); ( 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 )
; (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; verum