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;

hence PreNorms f is bounded_above by XXREAL_2:def 10; :: thesis: verum

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

A7:
X /\ (dom f) = X /\ X
by FUNCT_2:def 1;|.(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;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

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

r <= p

p is UpperBound of PreNorms f
by A8, XXREAL_2:def 1;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;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

hence PreNorms f is bounded_above by XXREAL_2:def 10; :: thesis: verum