let A be non empty set ; :: thesis: for h, f 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 h, f 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) )
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 h = (RealFuncExtMult A) . [a,f] ; :: thesis: for x being Element of A holds h . x = a * (f . x)
then Z: h = (RealFuncExtMult A) . a,f ;
let x be Element of A; :: thesis: h . x = a * (f . x)
thus h . x = (multreal [;] a,f) . x by Z, Def4
.= multreal . a,(f . x) by FUNCOP_1:66
.= a * (f . x) by BINOP_2:def 11 ; :: thesis: verum

end;

now

assume A1: 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) . [a,f]) . x

proof

B: multreal [;] a,f = (RealFuncExtMult A) . a,f by Def4;
let x be Element of A; :: thesis: h . x = ((RealFuncExtMult A) . [a,f]) . x
thus h . x = a * (f . x) by A1
.= multreal . a,(f . x) by BINOP_2:def 11
.= ((RealFuncExtMult A) . [a,f]) . x by B, FUNCOP_1:66 ; :: thesis: verum

end;

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

end;

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