let f, g be Linear_Combination of W; :: thesis: ( Carrier f c= T .: (Carrier l) & ( for w being Element of W holds f . w = Sum (lCFST (l,T,w)) ) & Carrier g c= T .: (Carrier l) & ( for w being Element of W holds g . w = Sum (lCFST (l,T,w)) ) implies f = g )

assume that

A16: ( Carrier f c= T .: (Carrier l) & ( for w being Element of W holds f . w = Sum (lCFST (l,T,w)) ) ) and

A17: ( Carrier g c= T .: (Carrier l) & ( for w being Element of W holds g . w = Sum (lCFST (l,T,w)) ) ) ; :: thesis: f = g

A18: for x being object st x in dom f holds

f . x = g . x

hence f = g by A18; :: thesis: verum

assume that

A16: ( Carrier f c= T .: (Carrier l) & ( for w being Element of W holds f . w = Sum (lCFST (l,T,w)) ) ) and

A17: ( Carrier g c= T .: (Carrier l) & ( for w being Element of W holds g . w = Sum (lCFST (l,T,w)) ) ) ; :: thesis: f = g

A18: for x being object st x in dom f holds

f . x = g . x

proof

( dom f = [#] W & dom g = [#] W )
by FUNCT_2:92;
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 (lCFST (l,T,x)) by A16;

hence f . x = g . x by A17; :: thesis: verum

end;assume x in dom f ; :: thesis: f . x = g . x

then reconsider x = x as Element of W ;

f . x = Sum (lCFST (l,T,x)) by A16;

hence f . x = g . x by A17; :: thesis: verum

hence f = g by A18; :: thesis: verum