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

reconsider K = L, K9 = L9 as Function of the carrier of V, the carrier of GF ;

assume that

A1: Carrier L = {} and

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

reconsider K = L, K9 = L9 as Function of the carrier of V, the carrier of GF ;

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

K . x = K9 . x

hence
L = L9
by FUNCT_2:12; :: thesis: verumK . x = K9 . x

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

assume x in the carrier of V ; :: thesis: K . x = K9 . x

then reconsider v = x as Element of V ;

end;assume x in the carrier of V ; :: thesis: K . x = K9 . x

then reconsider v = x as Element of V ;

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

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

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

hence contradiction by A2; :: thesis: verum

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

hence contradiction by A2; :: thesis: verum

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

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

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

hence contradiction by A1; :: thesis: verum

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

hence contradiction by A1; :: thesis: verum