let R be Ring; :: thesis:
let V be LeftMod of R; :: thesis:
let A be Subset of V; :: thesis:
let l be Linear_Combination of A; :: thesis:
let x be Element of V; :: thesis:
let a be Element of R; :: thesis:
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

let v be Element of V; :: thesis:
assume A7: not v in (Carrier l) \/ {x} ; :: thesis:
not v in {x} by A7, XBOOLE_0:def 3;
then v <> x by TARSKI:def 1;
then A8: m . v = l . v by FUNCT_7:32;
not v in Carrier l by A7, XBOOLE_0:def 3;
hence m . v = 0. R by A8; :: thesis:

end;

then reconsider m = m as Linear_Combination of V by VECTSP_6:def 1;
A9: Carrier m c= (Carrier l) \/ {x}

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in Carrier m ; :: thesis:
then consider z being Element of V such that
A10: y = z and
A11: m . z <> 0. R ;

suppose A12: z = x ; :: thesis:

( x in {x} & {x} c= (Carrier l) \/ {x} ) by TARSKI:def 1, XBOOLE_1:7;
hence y in (Carrier l) \/ {x} by A10, A12; :: thesis:

end;

suppose z <> x ; :: thesis:

then m . z = l . z by FUNCT_7:32;
then A13: z in Carrier l by A11;
Carrier l c= (Carrier l) \/ {x} by XBOOLE_1:7;
hence y in (Carrier l) \/ {x} by A10, A13; :: thesis:

end;

end;

end;

(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; :: thesis: