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 :: thesis: for x being Element of X holds ((FuncExtMult (X,Y)) . [jj,f]) . x = f . x

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

end;

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