let f, g be Linear_Combination of W; :: thesis: ( ( for w being Element of W holds f . w = Sum (l .: (T " {w})) ) & ( for w being Element of W holds g . w = Sum (l .: (T " {w})) ) implies f = g )
assume that
A18: for w being Element of W holds f . w = Sum (l .: (T " {w})) and
A19: for w being Element of W holds g . w = Sum (l .: (T " {w})) ; :: thesis: f = g
A20: for x being object st x in dom f holds
f . x = g . x

proof

let x be object ; :: thesis: ( x in dom f implies f . x = g . x )
assume x in dom f ; :: thesis: f . x = g . x
then reconsider x = x as Element of W ;
f . x = Sum (l .: (T " {x})) by A18;
hence f . x = g . x by A19; :: thesis: verum

end;

( dom f = [#] W & dom g = [#] W ) by FUNCT_2:92;
hence f = g by A20; :: thesis: verum