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))) by Lm3;
A2: dom (lmlt (p,(R1 + R2))) = (dom p) /\ (dom (R1 + R2)) by Lm1;
A3: dom (R1 + R2) = (dom R1) /\ (dom R2) by Lm3;
A4: dom (lmlt (p,R1)) = (dom p) /\ (dom R1) by Lm1;
A5: dom (lmlt (p,R2)) = (dom p) /\ (dom R2) by Lm1;
then A6: dom ((lmlt (p,R1)) + (lmlt (p,R2))) = (((dom p) /\ (dom R1)) /\ (dom p)) /\ (dom R2) by A1, A4, XBOOLE_1:16
.= (((dom p) /\ (dom p)) /\ (dom R1)) /\ (dom R2) by XBOOLE_1:16
.= dom (lmlt (p,(R1 + R2))) by A3, A2, XBOOLE_1:16 ;

now :: thesis: for x being object st x in dom ((lmlt (p,R1)) + (lmlt (p,R2))) holds
((lmlt (p,R1)) + (lmlt (p,R2))) . x = (lmlt (p,(R1 + R2))) . x

let x be object ; :: thesis: ( x in dom ((lmlt (p,R1)) + (lmlt (p,R2))) implies ((lmlt (p,R1)) + (lmlt (p,R2))) . x = (lmlt (p,(R1 + R2))) . x )
assume A7: x in dom ((lmlt (p,R1)) + (lmlt (p,R2))) ; :: thesis: ((lmlt (p,R1)) + (lmlt (p,R2))) . x = (lmlt (p,(R1 + R2))) . x
A8: x in dom (lmlt (p,R2)) by A1, A7, XBOOLE_0:def 4;
then A9: (lmlt (p,R2)) /. x = (lmlt (p,R2)) . x by PARTFUN1:def 6;
x in dom R2 by A5, A8, XBOOLE_0:def 4;
then A10: R2 /. x = R2 . x by PARTFUN1:def 6;
A11: x in dom (R1 + R2) by A2, A6, A7, XBOOLE_0:def 4;
then A12: (R1 + R2) . x = (R1 + R2) /. x by PARTFUN1:def 6;
A13: x in dom (lmlt (p,R1)) by A1, A7, XBOOLE_0:def 4;
then x in dom p by A4, XBOOLE_0:def 4;
then A14: p /. x = p . x by PARTFUN1:def 6;
x in dom R1 by A4, A13, XBOOLE_0:def 4;
then A15: R1 /. x = R1 . x by PARTFUN1:def 6;
A16: (lmlt (p,R1)) /. x = (lmlt (p,R1)) . x by A13, PARTFUN1:def 6;
hence ((lmlt (p,R1)) + (lmlt (p,R2))) . x = ((lmlt (p,R1)) /. x) + ((lmlt (p,R2)) /. x) by A7, A9, FVSUM_1:17
.= ( the lmult of V1 . ((p /. x),(R1 /. x))) + ((lmlt (p,R2)) /. x) by A13, A16, A14, A15, FUNCOP_1:22
.= ((p /. x) * (R1 /. x)) + ((p /. x) * (R2 /. x)) by A8, A9, A14, A10, FUNCOP_1:22
.= (p /. x) * ((R1 /. x) + (R2 /. x)) by VECTSP_1:def 14
.= (p /. x) * ((R1 + R2) /. x) by A11, A15, A10, A12, FVSUM_1:17
.= (lmlt (p,(R1 + R2))) . x by A6, A7, A14, A12, FUNCOP_1:22 ;
:: thesis: verum

end;

hence lmlt (p,(R1 + R2)) = (lmlt (p,R1)) + (lmlt (p,R2)) by A6; :: thesis: verum