let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for R1, R2 being FinSequence of V1
for p being FinSequence of K holds lmlt p,(R1 + R2) = (lmlt p,R1) + (lmlt p,R2)
let V1 be finite-dimensional VectSp of K; :: thesis: for R1, R2 being FinSequence of V1
for p being FinSequence of K holds lmlt p,(R1 + R2) = (lmlt p,R1) + (lmlt p,R2)
let R1, R2 be FinSequence of V1; :: thesis: for p being FinSequence of K holds lmlt p,(R1 + R2) = (lmlt p,R1) + (lmlt p,R2)
let p be FinSequence of K; :: thesis: lmlt p,(R1 + R2) = (lmlt p,R1) + (lmlt p,R2)
set L12 = lmlt p,(R1 + R2);
set L1 = lmlt p,R1;
set L2 = lmlt p,R2;
A1: ( dom ((lmlt p,R1) + (lmlt p,R2)) = (dom (lmlt p,R1)) /\ (dom (lmlt p,R2)) & dom (lmlt p,R1) = (dom p) /\ (dom R1) & dom (lmlt p,R2) = (dom p) /\ (dom R2) & dom (R1 + R2) = (dom R1) /\ (dom R2) & dom (lmlt p,(R1 + R2)) = (dom p) /\ (dom (R1 + R2)) ) by Lm1, Lm3;
A2: dom ((lmlt p,R1) + (lmlt p,R2)) = (((dom p) /\ (dom R1)) /\ (dom p)) /\ (dom R2) by A1, XBOOLE_1:16
.= (((dom p) /\ (dom p)) /\ (dom R1)) /\ (dom R2) by XBOOLE_1:16
.= dom (lmlt p,(R1 + R2)) by A1, XBOOLE_1:16 ;

now

let x be set ; :: thesis: ( x in dom ((lmlt p,R1) + (lmlt p,R2)) implies ((lmlt p,R1) + (lmlt p,R2)) . x = (lmlt p,(R1 + R2)) . x )
assume A3: x in dom ((lmlt p,R1) + (lmlt p,R2)) ; :: thesis: ((lmlt p,R1) + (lmlt p,R2)) . x = (lmlt p,(R1 + R2)) . x
A4: ( x in dom (lmlt p,R1) & x in dom (lmlt p,R2) & x in dom (R1 + R2) ) by A1, A2, A3, XBOOLE_0:def 4;
then ( x in dom p & x in dom R1 & x in dom R2 ) by A1, XBOOLE_0:def 4;
then A5: ( (lmlt p,R1) /. x = (lmlt p,R1) . x & (lmlt p,R2) /. x = (lmlt p,R2) . x & p /. x = p . x & R1 /. x = R1 . x & R2 /. x = R2 . x & (R1 + R2) . x = (R1 + R2) /. x ) by A4, PARTFUN1:def 8;
thus ((lmlt p,R1) + (lmlt p,R2)) . x = ((lmlt p,R1) /. x) + ((lmlt p,R2) /. x) by A5, A3, FVSUM_1:21
.= (the lmult of V1 . (p /. x),(R1 /. x)) + ((lmlt p,R2) /. x) by A5, A4, FUNCOP_1:28
.= ((p /. x) * (R1 /. x)) + ((p /. x) * (R2 /. x)) by A5, A4, FUNCOP_1:28
.= (p /. x) * ((R1 /. x) + (R2 /. x)) by VECTSP_1:def 26
.= (p /. x) * ((R1 + R2) /. x) by A4, A5, FVSUM_1:21
.= (lmlt p,(R1 + R2)) . x by A2, A5, A3, FUNCOP_1:28 ; :: thesis: verum

end;

hence lmlt p,(R1 + R2) = (lmlt p,R1) + (lmlt p,R2) by A2, FUNCT_1:9; :: thesis: verum