let F be Field; :: thesis: for V being VectSp of F
for l being Linear_Combination of V holds l = l ! ()

let V be VectSp of F; :: thesis: for l being Linear_Combination of V holds l = l ! ()
let l be Linear_Combination of V; :: thesis: l = l ! ()
set f = l | ();
set g = (V \ ()) --> (0. F);
set m = (l | ()) +* ((V \ ()) --> (0. F));
A2: dom l = [#] V by FUNCT_2:92;
then dom (l | ()) = Carrier l by RELAT_1:62;
then A3: (dom (l | ())) \/ (dom ((V \ ()) --> (0. F))) = [#] V by XBOOLE_1:45;
A4: for x being object st x in dom l holds
l . x = ((l | ()) +* ((V \ ()) --> (0. F))) . x
proof
let x be object ; :: thesis: ( x in dom l implies l . x = ((l | ()) +* ((V \ ()) --> (0. F))) . x )
assume x in dom l ; :: thesis: l . x = ((l | ()) +* ((V \ ()) --> (0. F))) . x
then reconsider x = x as Element of V ;
per cases ( x in Carrier l or not x in Carrier l ) ;
suppose A5: x in Carrier l ; :: thesis: l . x = ((l | ()) +* ((V \ ()) --> (0. F))) . x
then not x in dom ((V \ ()) --> (0. F)) by XBOOLE_0:def 5;
then ((l | ()) +* ((V \ ()) --> (0. F))) . x = (l | ()) . x by ;
hence l . x = ((l | ()) +* ((V \ ()) --> (0. F))) . x by ; :: thesis: verum
end;
suppose A6: not x in Carrier l ; :: thesis: l . x = ((l | ()) +* ((V \ ()) --> (0. F))) . x
then x in V \ () by XBOOLE_0:def 5;
then ( ((l | ()) +* ((V \ ()) --> (0. F))) . x = ((V \ ()) --> (0. F)) . x & ((V \ ()) --> (0. F)) . x = 0. F ) by ;
hence l . x = ((l | ()) +* ((V \ ()) --> (0. F))) . x by A6; :: thesis: verum
end;
end;
end;
dom l = dom ((l | ()) +* ((V \ ()) --> (0. F))) by ;
hence l = l ! () by A4; :: thesis: verum