let F be Field; :: thesis: for V being VectSp of
for A being Subset of
for l being Linear_Combination of A
for x being Element of
for a being Element of holds l +* x,a is Linear_Combination of A \/ {x}
let V be VectSp of ; :: thesis: for A being Subset of
for l being Linear_Combination of A
for x being Element of
for a being Element of holds l +* x,a is Linear_Combination of A \/ {x}
let A be Subset of ; :: thesis: for l being Linear_Combination of A
for x being Element of
for a being Element of holds l +* x,a is Linear_Combination of A \/ {x}
let l be Linear_Combination of A; :: thesis: for x being Element of
for a being Element of holds l +* x,a is Linear_Combination of A \/ {x}
let x be Element of ; :: thesis: for a being Element of holds l +* x,a is Linear_Combination of A \/ {x}
let a be Element of ; :: thesis: l +* x,a is Linear_Combination of A \/ {x}
set m = l +* x,a;
A1: dom (l +* x,a) = [#] V by FUNCT_2:def 1;
rng (l +* x,a) c= [#] F

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (l +* x,a) or y in [#] F )
assume y in rng (l +* x,a) ; :: thesis: y in [#] F
then consider x' being set such that
A2: x' in dom (l +* x,a) and
A3: (l +* x,a) . x' = y by FUNCT_1:def 5;
A4: x' in dom l by A1, A2, FUNCT_2:169;

per cases ( x' = x or x' <> x ) ;

suppose x' = x ; :: thesis: y in [#] F

then (l +* x,a) . x' = a by A4, FUNCT_7:33;
hence y in [#] F by A3; :: thesis: verum

end;

suppose A5: x' <> x ; :: thesis: y in [#] F

A6: ( l . x' in rng l & rng l c= [#] F ) by A4, FUNCT_1:12, FUNCT_2:169;
(l +* x,a) . x' = l . x' by A5, FUNCT_7:34;
hence y in [#] F by A3, A6; :: thesis: verum

end;

end;

end;

then reconsider m = l +* x,a as Element of Funcs ([#] V),([#] F) by A1, FUNCT_2:def 2;
set T = (Carrier l) \/ {x};
for v being Element of st not v in (Carrier l) \/ {x} holds
m . v = 0. F

proof

let v be Element of ; :: thesis: ( not v in (Carrier l) \/ {x} implies m . v = 0. F )
assume A7: not v in (Carrier l) \/ {x} ; :: thesis: m . v = 0. F
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:34;
not v in Carrier l by A7, XBOOLE_0:def 3;
hence m . v = 0. F by A8; :: thesis: verum

end;

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

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Carrier m or y in (Carrier l) \/ {x} )
assume y in Carrier m ; :: thesis: y in (Carrier l) \/ {x}
then consider z being Element of such that
A10: y = z and
A11: m . z <> 0. F ;

per cases ( z = x or z <> x ) ;

suppose A12: z = x ; :: thesis: y in (Carrier l) \/ {x}

( 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: verum

end;

suppose z <> x ; :: thesis: y in (Carrier l) \/ {x}

then m . z = l . z by FUNCT_7:34;
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: verum

end;

end;

end;

Carrier l c= A by VECTSP_6:def 7;
then (Carrier l) \/ {x} c= A \/ {x} by XBOOLE_1:9;
then Carrier m c= A \/ {x} by A9, XBOOLE_1:1;
hence l +* x,a is Linear_Combination of A \/ {x} by VECTSP_6:def 7; :: thesis: verum