let g1, g2 be Linear_Combination of rng f; :: thesis: ( ( for v being Element of V holds g1 . v = Sum (Expand (f,l,v)) ) & ( for v being Element of V holds g2 . v = Sum (Expand (f,l,v)) ) implies g1 = g2 )
assume that
A18: for w being Element of V holds g1 . w = Sum (Expand (f,l,w)) and
A19: for w being Element of V holds g2 . w = Sum (Expand (f,l,w)) ; :: thesis: g1 = g2
A20: for x being object st x in dom g1 holds
g1 . x = g2 . x

proof

let x be object ; :: thesis: ( x in dom g1 implies g1 . x = g2 . x )
assume x in dom g1 ; :: thesis: g1 . x = g2 . x
then reconsider x = x as Element of V ;
H: ( Carrier g1 c= rng f & Carrier g2 c= rng f ) by VECTSP_6:def 4;

per cases ( x in rng f or not x in rng f ) ;

suppose x in rng f ; :: thesis: g1 . x = g2 . x

g1 . x = Sum (Expand (f,l,x)) by A18;
hence g1 . x = g2 . x by A19; :: thesis: verum

end;

suppose A21: not x in rng f ; :: thesis: g1 . x = g2 . x

then g1 . x = 0. F by H, VECTSP_6:2
.= g2 . x by A21, H, VECTSP_6:2 ;
hence g1 . x = g2 . x ; :: thesis: verum

end;

end;

end;

( dom g1 = [#] V & dom g2 = [#] V ) by FUNCT_2:92;
hence g1 = g2 by A20; :: thesis: verum