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

now

let x be Element of X; :: thesis: ((FuncExtMult X,Y) . [1,f]) . x = f . x
thus ((FuncExtMult X,Y) . [1,f]) . x = 1 * (f . x) by Th5
.= f . x by RLVECT_1:def 9 ; :: thesis: verum

end;

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