let X be non empty set ; 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; 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); (FuncExtMult (X,Y)) . [1,f] = f
hence
(FuncExtMult (X,Y)) . [1,f] = f
by FUNCT_2:63; verum