let K be Field; 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; 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; 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; 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)))
by Lm3;
A2:
dom (lmlt ((p1 + p2),R)) = (dom (p1 + p2)) /\ (dom R)
by Lm1;
A3:
dom (lmlt (p1,R)) = (dom p1) /\ (dom R)
by Lm1;
A4:
dom (lmlt (p2,R)) = (dom p2) /\ (dom R)
by Lm1;
then A5: dom ((lmlt (p1,R)) + (lmlt (p2,R))) =
(((dom p1) /\ (dom R)) /\ (dom p2)) /\ (dom R)
by A1, A3, 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 A2, Lm2
;
now for x being object st x in dom ((lmlt (p1,R)) + (lmlt (p2,R))) holds
((lmlt (p1,R)) + (lmlt (p2,R))) . x = (lmlt ((p1 + p2),R)) . xlet x be
object ;
( x in dom ((lmlt (p1,R)) + (lmlt (p2,R))) implies ((lmlt (p1,R)) + (lmlt (p2,R))) . x = (lmlt ((p1 + p2),R)) . x )assume A6:
x in dom ((lmlt (p1,R)) + (lmlt (p2,R)))
;
((lmlt (p1,R)) + (lmlt (p2,R))) . x = (lmlt ((p1 + p2),R)) . xA7:
x in dom (lmlt (p2,R))
by A1, A6, XBOOLE_0:def 4;
then A8:
(lmlt (p2,R)) /. x = (lmlt (p2,R)) . x
by PARTFUN1:def 6;
x in dom p2
by A4, A7, XBOOLE_0:def 4;
then A9:
p2 /. x = p2 . x
by PARTFUN1:def 6;
A10:
x in dom (p1 + p2)
by A2, A5, A6, XBOOLE_0:def 4;
then A11:
(p1 + p2) . x = (p1 + p2) /. x
by PARTFUN1:def 6;
A12:
x in dom (lmlt (p1,R))
by A1, A6, XBOOLE_0:def 4;
then
x in dom p1
by A3, XBOOLE_0:def 4;
then A13:
p1 /. x = p1 . x
by PARTFUN1:def 6;
x in dom R
by A3, A12, XBOOLE_0:def 4;
then A14:
R /. x = R . x
by PARTFUN1:def 6;
A15:
(lmlt (p1,R)) /. x = (lmlt (p1,R)) . x
by A12, PARTFUN1:def 6;
hence ((lmlt (p1,R)) + (lmlt (p2,R))) . x =
((lmlt (p1,R)) /. x) + ((lmlt (p2,R)) /. x)
by A6, A8, FVSUM_1:17
.=
( the lmult of V1 . ((p1 /. x),(R /. x))) + ((lmlt (p2,R)) /. x)
by A12, A15, A13, A14, FUNCOP_1:22
.=
((p1 /. x) * (R /. x)) + ((p2 /. x) * (R /. x))
by A7, A8, A9, A14, FUNCOP_1:22
.=
((p1 /. x) + (p2 /. x)) * (R /. x)
by VECTSP_1:def 15
.=
((p1 + p2) /. x) * (R /. x)
by A10, A13, A9, A11, FVSUM_1:17
.=
(lmlt ((p1 + p2),R)) . x
by A5, A6, A14, A11, FUNCOP_1:22
;
verum end;
hence
lmlt ((p1 + p2),R) = (lmlt (p1,R)) + (lmlt (p2,R))
by A5; verum