let L, L9 be Linear_Combination of V; :: thesis: ( Carrier L = {} & Carrier L9 = {} implies L = L9 )

assume that

A1: Carrier L = {} and

A2: Carrier L9 = {} ; :: thesis: L = L9

assume that

A1: Carrier L = {} and

A2: Carrier L9 = {} ; :: thesis: L = L9

now :: thesis: for x being object st x in the carrier of V holds

L . x = L9 . x

hence
L = L9
; :: thesis: verumL . x = L9 . x

let x be object ; :: thesis: ( x in the carrier of V implies L . x = L9 . x )

assume x in the carrier of V ; :: thesis: L . x = L9 . x

then reconsider v = x as Element of V ;

end;assume x in the carrier of V ; :: thesis: L . x = L9 . x

then reconsider v = x as Element of V ;

A3: now :: thesis: not L9 . v <> 0

assume
L9 . v <> 0
; :: thesis: contradiction

then v in { u where u is Element of V : L9 . u <> 0 } ;

hence contradiction by A2; :: thesis: verum

end;then v in { u where u is Element of V : L9 . u <> 0 } ;

hence contradiction by A2; :: thesis: verum

now :: thesis: not L . v <> 0

hence
L . x = L9 . x
by A3; :: thesis: verumassume
L . v <> 0
; :: thesis: contradiction

then v in { u where u is Element of V : L . u <> 0 } ;

hence contradiction by A1; :: thesis: verum

end;then v in { u where u is Element of V : L . u <> 0 } ;

hence contradiction by A1; :: thesis: verum