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