let F be Field; :: thesis: for V being VectSp of F
for l being Linear_Combination of V holds l = l ! (Carrier l)
let V be VectSp of F; :: thesis: for l being Linear_Combination of V holds l = l ! (Carrier l)
let l be Linear_Combination of V; :: thesis: l = l ! (Carrier l)
set f = l | (Carrier l);
set g = (V \ (Carrier l)) --> (0. F);
set m = (l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F));
A1: dom l = [#] V by FUNCT_2:169;
then A2: dom (l | (Carrier l)) = Carrier l by RELAT_1:91;
A3: dom ((V \ (Carrier l)) --> (0. F)) = V \ (Carrier l) by FUNCOP_1:19;
then A4: (dom (l | (Carrier l))) \/ (dom ((V \ (Carrier l)) --> (0. F))) = [#] V by A2, XBOOLE_1:45;
then A5: dom l = dom ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) by A1, FUNCT_4:def 1;
for x being set st x in dom l holds
l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x

proof

let x be set ; :: thesis: ( x in dom l implies l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x )
assume A6: x in dom l ; :: thesis: l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x
reconsider x = x as Element of V by A6;

per cases ( x in Carrier l or not x in Carrier l ) ;

suppose A7: x in Carrier l ; :: thesis: l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x

then not x in dom ((V \ (Carrier l)) --> (0. F)) by XBOOLE_0:def 5;
then ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x = (l | (Carrier l)) . x by A4, FUNCT_4:def 1;
hence l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x by A7, FUNCT_1:72; :: thesis: verum

end;

suppose A8: not x in Carrier l ; :: thesis: l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x

then A9: x in V \ (Carrier l) by XBOOLE_0:def 5;
then A10: ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x = ((V \ (Carrier l)) --> (0. F)) . x by A3, A4, FUNCT_4:def 1;
((V \ (Carrier l)) --> (0. F)) . x = 0. F by A9, FUNCOP_1:13;
hence l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x by A8, A10; :: thesis: verum

end;

end;

end;

hence l = l ! (Carrier l) by A5, FUNCT_1:def 17; :: thesis: verum