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

for f being Element of Funcs (X, the carrier of Y) holds (FuncExtMult (X,Y)) . [1r,f] = f

let Y be ComplexLinearSpace; :: thesis: for f being Element of Funcs (X, the carrier of Y) holds (FuncExtMult (X,Y)) . [1r,f] = f

let f be Element of Funcs (X, the carrier of Y); :: thesis: (FuncExtMult (X,Y)) . [1r,f] = f

for f being Element of Funcs (X, the carrier of Y) holds (FuncExtMult (X,Y)) . [1r,f] = f

let Y be ComplexLinearSpace; :: thesis: for f being Element of Funcs (X, the carrier of Y) holds (FuncExtMult (X,Y)) . [1r,f] = f

let f be Element of Funcs (X, the carrier of Y); :: thesis: (FuncExtMult (X,Y)) . [1r,f] = f

now :: thesis: for x being Element of X holds ((FuncExtMult (X,Y)) . [1r,f]) . x = f . x

hence
(FuncExtMult (X,Y)) . [1r,f] = f
by FUNCT_2:63; :: thesis: verumlet x be Element of X; :: thesis: ((FuncExtMult (X,Y)) . [1r,f]) . x = f . x

thus ((FuncExtMult (X,Y)) . [1r,f]) . x = 1r * (f . x) by Th2

.= f . x by CLVECT_1:def 5 ; :: thesis: verum

end;thus ((FuncExtMult (X,Y)) . [1r,f]) . x = 1r * (f . x) by Th2

.= f . x by CLVECT_1:def 5 ; :: thesis: verum