let R be Ring; :: thesis: for V being LeftMod of R
for l being Linear_Combination of V holds l = l ! ()

let V be LeftMod of R; :: 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 = (() `) --> (0. R);
set m = (l | ()) +* ((() `) --> (0. R));
A2: dom l = [#] V by FUNCT_2:92;
then dom (l | ()) = Carrier l by RELAT_1:62;
then A3: (dom (l | ())) \/ (dom ((() `) --> (0. R))) = [#] V by XBOOLE_1:45;
for x being object st x in dom l holds
l . x = ((l | ()) +* ((() `) --> (0. R))) . x
proof
let x be object ; :: thesis: ( x in dom l implies l . x = ((l | ()) +* ((() `) --> (0. R))) . x )
assume x in dom l ; :: thesis: l . x = ((l | ()) +* ((() `) --> (0. R))) . 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 | ()) +* ((() `) --> (0. R))) . x
then not x in dom ((() `) --> (0. R)) by XBOOLE_0:def 5;
then ((l | ()) +* ((() `) --> (0. R))) . x = (l | ()) . x by ;
hence l . x = ((l | ()) +* ((() `) --> (0. R))) . x by ; :: thesis: verum
end;
suppose A6: not x in Carrier l ; :: thesis: l . x = ((l | ()) +* ((() `) --> (0. R))) . x
then x in () ` by XBOOLE_0:def 5;
then ( ((l | ()) +* ((() `) --> (0. R))) . x = ((() `) --> (0. R)) . x & ((() `) --> (0. R)) . x = 0. R ) by ;
hence l . x = ((l | ()) +* ((() `) --> (0. R))) . x by A6; :: thesis: verum
end;
end;
end;
hence l = l ! () by A2; :: thesis: verum