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

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 Th3
.= f . x by CLVECT_1:def 2 ; :: thesis: verum

end;

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