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