let X be non empty set ; :: thesis: for Y being RealNormSpace
for f, h being Point of
for f', h' being bounded Function of X,the carrier of Y st f' = f & h' = h holds
for a being Real holds
( h = a * f iff for x being Element of X holds h' . x = a * (f' . x) )
let Y be RealNormSpace; :: thesis: for f, h being Point of
for f', h' being bounded Function of X,the carrier of Y st f' = f & h' = h holds
for a being Real holds
( h = a * f iff for x being Element of X holds h' . x = a * (f' . x) )
let f, h be Point of ; :: thesis: for f', h' being bounded Function of X,the carrier of Y st f' = f & h' = h holds
for a being Real holds
( h = a * f iff for x being Element of X holds h' . x = a * (f' . x) )
let f', h' be bounded Function of X,the carrier of Y; :: thesis: ( f' = f & h' = h implies for a being Real holds
( h = a * f iff for x being Element of X holds h' . x = a * (f' . x) ) )
assume A1: ( f' = f & h' = h ) ; :: thesis: for a being Real holds
( h = a * f iff for x being Element of X holds h' . x = a * (f' . x) )
reconsider h1 = h as VECTOR of ;
reconsider f1 = f as VECTOR of ;
let a be Real; :: thesis: ( h = a * f iff for x being Element of X holds h' . x = a * (f' . x) )
( h = a * f iff h1 = a * f1 ) ;
hence ( h = a * f iff for x being Element of X holds h' . x = a * (f' . x) ) by A1, Th11; :: thesis: verum