let R be Ring; for V being LeftMod of R
for A being Subset of V
for l being Linear_Combination of A
for x being Element of V
for a being Element of R holds l +* (x,a) is Linear_Combination of A \/ {x}
let V be LeftMod of R; for A being Subset of V
for l being Linear_Combination of A
for x being Element of V
for a being Element of R holds l +* (x,a) is Linear_Combination of A \/ {x}
let A be Subset of V; for l being Linear_Combination of A
for x being Element of V
for a being Element of R holds l +* (x,a) is Linear_Combination of A \/ {x}
let l be Linear_Combination of A; for x being Element of V
for a being Element of R holds l +* (x,a) is Linear_Combination of A \/ {x}
let x be Element of V; for a being Element of R holds l +* (x,a) is Linear_Combination of A \/ {x}
let a be Element of R; l +* (x,a) is Linear_Combination of A \/ {x}
set m = l +* (x,a);
A1: dom (l +* (x,a)) =
dom l
by FUNCT_7:30
.=
[#] V
by FUNCT_2:def 1
;
rng (l +* (x,a)) c= the carrier of R
;
then reconsider m = l +* (x,a) as Element of Funcs (([#] V), the carrier of R) by A1, FUNCT_2:def 2;
set T = (Carrier l) \/ {x};
for v being Element of V st not v in (Carrier l) \/ {x} holds
m . v = 0. R
then reconsider m = m as Linear_Combination of V by VECTSP_6:def 1;
A9:
Carrier m c= (Carrier l) \/ {x}
(Carrier l) \/ {x} c= A \/ {x}
by XBOOLE_1:9, VECTSP_6:def 4;
then
Carrier m c= A \/ {x}
by A9;
hence
l +* (x,a) is Linear_Combination of A \/ {x}
by VECTSP_6:def 4; verum