let A be non empty set ; :: thesis: for f, h being Element of Funcs (A,REAL)
for a being Real holds
( h = (RealFuncExtMult A) . [a,f] iff for x being Element of A holds h . x = a * (f . x) )
let f, h be Element of Funcs (A,REAL); :: thesis: for a being Real holds
( h = (RealFuncExtMult A) . [a,f] iff for x being Element of A holds h . x = a * (f . x) )
let a be Real; :: thesis: ( h = (RealFuncExtMult A) . [a,f] iff for x being Element of A holds h . x = a * (f . x) )
reconsider aa = a as Element of REAL by XREAL_0:def 1;
thus ( h = (RealFuncExtMult A) . [a,f] implies for x being Element of A holds h . x = a * (f . x) ) :: thesis: ( ( for x being Element of A holds h . x = a * (f . x) ) implies h = (RealFuncExtMult A) . [a,f] )

proof

assume A1: h = (RealFuncExtMult A) . [a,f] ; :: thesis: for x being Element of A holds h . x = a * (f . x)
let x be Element of A; :: thesis: h . x = a * (f . x)
h = (RealFuncExtMult A) . (a,f) by A1;
hence h . x = (multreal [;] (aa,f)) . x by Def3
.= multreal . (aa,(f . x)) by FUNCOP_1:53
.= a * (f . x) by BINOP_2:def 11 ;
:: thesis: verum

end;

now :: thesis: ( ( for x being Element of A holds h . x = a * (f . x) ) implies h = (RealFuncExtMult A) . (a,f) )

assume A2: for x being Element of A holds h . x = a * (f . x) ; :: thesis: h = (RealFuncExtMult A) . (a,f)
for x being Element of A holds h . x = ((RealFuncExtMult A) . [aa,f]) . x

proof

let x be Element of A; :: thesis: h . x = ((RealFuncExtMult A) . [aa,f]) . x
A3: multreal [;] (a,f) = (RealFuncExtMult A) . (a,f) by Def3;
thus h . x = a * (f . x) by A2
.= multreal . (a,(f . x)) by BINOP_2:def 11
.= ((RealFuncExtMult A) . [aa,f]) . x by A3, FUNCOP_1:53 ; :: thesis: verum

end;

hence h = (RealFuncExtMult A) . (a,f) by FUNCT_2:63; :: thesis: verum

end;

hence ( ( for x being Element of A holds h . x = a * (f . x) ) implies h = (RealFuncExtMult A) . [a,f] ) ; :: thesis: verum