let X be non empty set ; 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; 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)); 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; ( 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 ( ( for x being Element of X holds h . x = c * (f . x) ) implies h = c * f )
end;
assume
for x being Element of X holds h . x = c * (f . x)
; h = c * f
then
h9 = (FuncExtMult (X,Y)) . [c,f9]
by Th2;
hence
h = c * f
by CLVECT_1:def 1; verum