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

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

let 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;

hence (FuncExtMult (X,Y)) . [1r,f] = f by FUNCT_2:63; :: thesis: verum