let A be non empty set ; :: thesis: for f being Element of Funcs (A,REAL)
for a being Real holds (RealFuncExtMult A) . (a,f) = a (#) f
let f be Element of Funcs (A,REAL); :: thesis: for a being Real holds (RealFuncExtMult A) . (a,f) = a (#) f
let a be Real; :: thesis: (RealFuncExtMult A) . (a,f) = a (#) f
reconsider aa = a as Element of REAL by XREAL_0:def 1;
set h = (RealFuncExtMult A) . (a,f);
b1: dom (a (#) f) = dom f by VALUED_1:def 5
.= A by FUNCT_2:def 1 ;
A2: now :: thesis: for x being Element of A holds ((RealFuncExtMult A) . (a,f)) . x = (a (#) f) . x
let x be Element of A; :: thesis: ((RealFuncExtMult A) . (a,f)) . x = (a (#) f) . x
thus ((RealFuncExtMult A) . (a,f)) . x = (multreal [;] (aa,f)) . x by Def3
.= multreal . (aa,(f . x)) by FUNCOP_1:53
.= a * (f . x) by BINOP_2:def 11
.= (a (#) f) . x by VALUED_1:def 5, b1 ; :: thesis: verum
end;
( a in REAL & f in Funcs (A,REAL) ) by XREAL_0:def 1;
then [a,f] in [:REAL,(Funcs (A,REAL)):] by ZFMISC_1:87;
then (RealFuncExtMult A) . (a,f) is Function of A,REAL by FUNCT_2:66, FUNCT_2:5;
then B1: dom ((RealFuncExtMult A) . (a,f)) = A by FUNCT_2:def 1;
for x being object st x in dom (a (#) f) holds
((RealFuncExtMult A) . (a,f)) . x = (a (#) f) . x by A2, b1;
hence (RealFuncExtMult A) . (a,f) = a (#) f by FUNCT_1:2, B1, b1; :: thesis: verum