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

now

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

end;

hence lmlt (p1 + p2),R = (lmlt p1,R) + (lmlt p2,R) by A2, FUNCT_1:9; :: thesis: verum