let X be non empty set ; :: thesis: for Y being RealLinearSpace
for f, h being Element of Funcs (X, the carrier of Y)
for a being Real holds
( h = (FuncExtMult (X,Y)) . [a,f] iff for x being Element of X holds h . x = a * (f . x) )
let Y be RealLinearSpace; :: thesis: for f, h being Element of Funcs (X, the carrier of Y)
for a being Real holds
( h = (FuncExtMult (X,Y)) . [a,f] iff for x being Element of X holds h . x = a * (f . x) )
let f, h be Element of Funcs (X, the carrier of Y); :: thesis: for a being Real holds
( h = (FuncExtMult (X,Y)) . [a,f] iff for x being Element of X holds h . x = a * (f . x) )
let a be Real; :: thesis: ( h = (FuncExtMult (X,Y)) . [a,f] iff for x being Element of X holds h . x = a * (f . x) )
thus ( h = (FuncExtMult (X,Y)) . [a,f] implies for x being Element of X holds h . x = a * (f . x) ) by Def2; :: thesis: ( ( for x being Element of X holds h . x = a * (f . x) ) implies h = (FuncExtMult (X,Y)) . [a,f] )
reconsider a = a as Element of REAL by XREAL_0:def 1;

now :: thesis: ( ( for x being Element of X holds h . x = a * (f . x) ) implies h = (FuncExtMult (X,Y)) . [a,f] )

assume A1: for x being Element of X holds h . x = a * (f . x) ; :: thesis: h = (FuncExtMult (X,Y)) . [a,f]
for x being Element of X holds h . x = ((FuncExtMult (X,Y)) . [a,f]) . x

proof

let x be Element of X; :: thesis: h . x = ((FuncExtMult (X,Y)) . [a,f]) . x
thus h . x = a * (f . x) by A1
.= ((FuncExtMult (X,Y)) . [a,f]) . x by Def2 ; :: thesis: verum

end;

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

end;

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