consider A being non empty set , x1, x2 being set such that

A1: ( A = {x1,x2} & x1 <> x2 ) by Lm3;

take V = ComplexVectSpace A; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( ( 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; :: thesis: 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) :: thesis: verum

A1: ( A = {x1,x2} & x1 <> x2 ) by Lm3;

take V = ComplexVectSpace A; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( ( 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; :: thesis: 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) :: thesis: verum

proof

let w be VECTOR of V; :: thesis: ex a, b being Complex st w = (a * u) + (b * v)

reconsider h = w as Element of Funcs (A,COMPLEX) ;

consider a, b being Complex such that

A4: h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) by A3;

h = (a * u) + (b * v) by A4;

hence ex a, b being Complex st w = (a * u) + (b * v) ; :: thesis: verum

end;reconsider h = w as Element of Funcs (A,COMPLEX) ;

consider a, b being Complex such that

A4: h = (ComplexFuncAdd A) . (((ComplexFuncExtMult A) . [a,f]),((ComplexFuncExtMult A) . [b,g])) by A3;

h = (a * u) + (b * v) by A4;

hence ex a, b being Complex st w = (a * u) + (b * v) ; :: thesis: verum