let X be non empty set ; :: thesis: for Y being ComplexLinearSpace

for f, h being VECTOR of (ComplexVectSpace (X,Y))

for c being Complex holds

( h = c * f iff for x being Element of X holds h . x = c * (f . x) )

let Y be ComplexLinearSpace; :: thesis: for f, h being VECTOR of (ComplexVectSpace (X,Y))

for c being Complex holds

( h = c * f iff for x being Element of X holds h . x = c * (f . x) )

let f, h be VECTOR of (ComplexVectSpace (X,Y)); :: thesis: for c being Complex holds

( h = c * f iff for x being Element of X holds h . x = c * (f . x) )

let c be Complex; :: thesis: ( h = c * f iff for x being Element of X holds h . x = c * (f . x) )

reconsider f9 = f, h9 = h as Element of Funcs (X, the carrier of Y) ;

then h9 = (FuncExtMult (X,Y)) . [c,f9] by Th2;

hence h = c * f by CLVECT_1:def 1; :: thesis: verum

for f, h being VECTOR of (ComplexVectSpace (X,Y))

for c being Complex holds

( h = c * f iff for x being Element of X holds h . x = c * (f . x) )

let Y be ComplexLinearSpace; :: thesis: for f, h being VECTOR of (ComplexVectSpace (X,Y))

for c being Complex holds

( h = c * f iff for x being Element of X holds h . x = c * (f . x) )

let f, h be VECTOR of (ComplexVectSpace (X,Y)); :: thesis: for c being Complex holds

( h = c * f iff for x being Element of X holds h . x = c * (f . x) )

let c be Complex; :: thesis: ( h = c * f iff for x being Element of X holds h . x = c * (f . x) )

reconsider f9 = f, h9 = h as Element of Funcs (X, the carrier of Y) ;

hereby :: thesis: ( ( for x being Element of X holds h . x = c * (f . x) ) implies h = c * f )

assume
for x being Element of X holds h . x = c * (f . x)
; :: thesis: h = c * fassume A1:
h = c * f
; :: thesis: for x being Element of X holds h . x = c * (f . x)

let x be Element of X; :: thesis: h . x = c * (f . x)

h = (FuncExtMult (X,Y)) . [c,f9] by A1, CLVECT_1:def 1;

hence h . x = c * (f . x) by Th2; :: thesis: verum

end;let x be Element of X; :: thesis: h . x = c * (f . x)

h = (FuncExtMult (X,Y)) . [c,f9] by A1, CLVECT_1:def 1;

hence h . x = c * (f . x) by Th2; :: thesis: verum

then h9 = (FuncExtMult (X,Y)) . [c,f9] by Th2;

hence h = c * f by CLVECT_1:def 1; :: thesis: verum