let X be non empty set ; :: thesis: for f being Function of X,COMPLEX st f | X is bounded holds
PreNorms f is bounded_above
let f be Function of X,COMPLEX; :: thesis: ( f | X is bounded implies PreNorms f is bounded_above )
A1: dom |.f.| = dom f by VALUED_1:def 11;
A2: dom (|.f.| | X) = X /\ (dom |.f.|) by RELAT_1:61;
A3: |.f.| | X = |.(f | X).| by RFUNCT_1:46;
assume f | X is bounded ; :: thesis: PreNorms f is bounded_above
then |.f.| | X is bounded by A3, Lm2;
then consider p being Real such that
A4: for c being object st c in dom (|.f.| | X) holds
|.((|.f.| | X) . c).| <= p by RFUNCT_1:72;

A5: now :: thesis: for c being Element of X st c in X /\ (dom f) holds
|.(f . c).| <= p

let c be Element of X; :: thesis: ( c in X /\ (dom f) implies |.(f . c).| <= p )
assume A6: c in X /\ (dom f) ; :: thesis: |.(f . c).| <= p
|.((|.f.| | X) . c).| = |.(|.f.| . c).| by A1, A2, A6, FUNCT_1:47
.= |.|.(f . c).|.| by VALUED_1:18 ;
hence |.(f . c).| <= p by A1, A2, A4, A6; :: thesis: verum

end;

A7: X /\ (dom f) = X /\ X by FUNCT_2:def 1;

A8: now :: thesis: for r being ExtReal st r in PreNorms f holds
r <= p

let r be ExtReal; :: thesis: ( r in PreNorms f implies r <= p )
assume r in PreNorms f ; :: thesis: r <= p
then consider t being Element of X such that
A9: r = |.(f . t).| ;
thus r <= p by A7, A9, A5; :: thesis: verum

end;

p is UpperBound of PreNorms f by A8, XXREAL_2:def 1;
hence PreNorms f is bounded_above by XXREAL_2:def 10; :: thesis: verum