consider A being non empty set , x1, x2 being set such that
A1:
( A = {x1,x2} & x1 <> x2 )
by Lm3;
take V = ComplexVectSpace A; ex u, v being VECTOR of V st
( ( for a, b being Complex st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being VECTOR of V ex a, b being Complex st w = (a * u) + (b * v) ) )
consider f, g being Element of Funcs (A,COMPLEX) such that
A2:
for a, b being Complex st (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) = ComplexFuncZero A holds
( a = 0c & b = 0c )
and
A3:
for h being Element of Funcs (A,COMPLEX) ex a, b being Complex st h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g]))
by A1, Th22;
reconsider u = f, v = g as VECTOR of V ;
take
u
; ex v being VECTOR of V st
( ( for a, b being Complex st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being VECTOR of V ex a, b being Complex st w = (a * u) + (b * v) ) )
take
v
; ( ( for a, b being Complex st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) & ( for w being VECTOR of V ex a, b being Complex st w = (a * u) + (b * v) ) )
thus
for a, b being Complex st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 )
by A2; for w being VECTOR of V ex a, b being Complex st w = (a * u) + (b * v)
thus
for w being VECTOR of V ex a, b being Complex st w = (a * u) + (b * v)
verum