let A be non empty closed_interval Subset of REAL; :: thesis: for a, b being Real st A = [.a,b.] holds
ex x being Function of A,(BoundedFunctions A) st
for s being Real st s in [.a,b.] holds
( ( s = a implies x . s = [.a,b.] --> 0 ) & ( s <> a implies x . s = ([.a,s.] --> 1) +* (].s,b.] --> 0) ) )
let a, b be Real; :: thesis: ( A = [.a,b.] implies ex x being Function of A,(BoundedFunctions A) st
for s being Real st s in [.a,b.] holds
( ( s = a implies x . s = [.a,b.] --> 0 ) & ( s <> a implies x . s = ([.a,s.] --> 1) +* (].s,b.] --> 0) ) ) )
assume A2: A = [.a,b.] ; :: thesis: ex x being Function of A,(BoundedFunctions A) st
for s being Real st s in [.a,b.] holds
( ( s = a implies x . s = [.a,b.] --> 0 ) & ( s <> a implies x . s = ([.a,s.] --> 1) +* (].s,b.] --> 0) ) )
defpred S₁[ object ] means $1 = a;
deffunc H₁( object ) -> Element of bool [:[.a,b.],NAT:] = [.a,b.] --> 0;
deffunc H₂( object ) -> set = ([.a,(In ($1,REAL)).] --> 1) +* (].(In ($1,REAL)),b.] --> 0);
set B = BoundedFunctions A;
A3: for s being object st s in [.a,b.] holds
( ( S₁[s] implies H₁(s) in BoundedFunctions A ) & ( not S₁[s] implies H₂(s) in BoundedFunctions A ) )

proof

let s be object ; :: thesis: ( s in [.a,b.] implies ( ( S₁[s] implies H₁(s) in BoundedFunctions A ) & ( not S₁[s] implies H₂(s) in BoundedFunctions A ) ) )
assume A4: s in [.a,b.] ; :: thesis: ( ( S₁[s] implies H₁(s) in BoundedFunctions A ) & ( not S₁[s] implies H₂(s) in BoundedFunctions A ) )
then reconsider r = s as Real ;
thus ( S₁[s] implies H₁(s) in BoundedFunctions A ) :: thesis: ( not S₁[s] implies H₂(s) in BoundedFunctions A )

proof

assume S₁[s] ; :: thesis: H₁(s) in BoundedFunctions A
set f1 = [.a,b.] --> 0;
A7: dom ([.a,b.] --> 0) = A by A2, FUNCOP_1:13;
rng ([.a,b.] --> 0) c= REAL ;
then reconsider f = [.a,b.] --> 0 as Function of A,REAL by A7, FUNCT_2:2;
reconsider r0 = 0 as Real ;
for r being ExtReal st r in PreNorms f holds
r <= r0

proof

let r be ExtReal; :: thesis: ( r in PreNorms f implies r <= r0 )
assume r in PreNorms f ; :: thesis: r <= r0
then consider t being Element of A such that
A8: r = |.(f . t).| ;
f . t = 0 by A2, FUNCOP_1:7;
hence r <= r0 by A8; :: thesis: verum

end;

then r0 is UpperBound of PreNorms f by XXREAL_2:def 1;
then PreNorms f is bounded_above by XXREAL_2:def 10;
then f | A is bounded by C0SP1:18;
hence H₁(s) in BoundedFunctions A ; :: thesis: verum

end;

H₂(s) in BoundedFunctions A

proof

set g1 = [.a,(In (s,REAL)).] --> 1;
set g2 = ].(In (s,REAL)),b.] --> 0;
B9: ( a <= r & r <= b ) by A4, XXREAL_1:1;
A10: ( dom ([.a,(In (s,REAL)).] --> 1) = [.a,(In (s,REAL)).] & dom (].(In (s,REAL)),b.] --> 0) = ].(In (s,REAL)),b.] ) by FUNCOP_1:13;
then A11: (dom ([.a,(In (s,REAL)).] --> 1)) \/ (dom (].(In (s,REAL)),b.] --> 0)) = A by A2, B9, XXREAL_1:167;
then A12: dom (([.a,(In (s,REAL)).] --> 1) +* (].(In (s,REAL)),b.] --> 0)) = A by FUNCT_4:def 1;
rng (([.a,(In (s,REAL)).] --> 1) +* (].(In (s,REAL)),b.] --> 0)) c= REAL ;
then reconsider f = ([.a,(In (s,REAL)).] --> 1) +* (].(In (s,REAL)),b.] --> 0) as Function of A,REAL by A12, FUNCT_2:2;
reconsider r0 = 1 as Real ;
for c being object st c in (dom ([.a,(In (s,REAL)).] --> 1)) /\ (dom f) holds
|.(f . c).| <= r0

proof

let c be object ; :: thesis: ( c in (dom ([.a,(In (s,REAL)).] --> 1)) /\ (dom f) implies |.(f . c).| <= r0 )
assume c in (dom ([.a,(In (s,REAL)).] --> 1)) /\ (dom f) ; :: thesis: |.(f . c).| <= r0
then A16: c in dom ([.a,(In (s,REAL)).] --> 1) by FUNCT_4:10, XBOOLE_1:28;
then |.(([.a,(In (s,REAL)).] --> 1) . c).| = 1 by FUNCOP_1:7;
then |.((f | (dom ([.a,(In (s,REAL)).] --> 1))) . c).| = 1 by FUNCT_4:33, A10, XXREAL_1:90;
hence |.(f . c).| <= r0 by A16, FUNCT_1:49; :: thesis: verum

end;

then A17: f | (dom ([.a,(In (s,REAL)).] --> 1)) is bounded by RFUNCT_1:73;
reconsider s0 = 0 as Real ;
for c being object st c in (dom (].(In (s,REAL)),b.] --> 0)) /\ (dom f) holds
|.(f . c).| <= s0

proof

let c be object ; :: thesis: ( c in (dom (].(In (s,REAL)),b.] --> 0)) /\ (dom f) implies |.(f . c).| <= s0 )
assume c in (dom (].(In (s,REAL)),b.] --> 0)) /\ (dom f) ; :: thesis: |.(f . c).| <= s0
then A18: c in dom (].(In (s,REAL)),b.] --> 0) by FUNCT_4:10, XBOOLE_1:28;
then |.((].(In (s,REAL)),b.] --> 0) . c).| = 0 by FUNCOP_1:7;
then |.((f | (dom (].(In (s,REAL)),b.] --> 0))) . c).| = 0 by FUNCT_4:23;
hence |.(f . c).| <= s0 by A18, FUNCT_1:49; :: thesis: verum

end;

then f | (dom (].(In (s,REAL)),b.] --> 0)) is bounded by RFUNCT_1:73;
then f | A is bounded by A11, A17, RFUNCT_1:87;
hence H₂(s) in BoundedFunctions A ; :: thesis: verum

end;

hence ( not S₁[s] implies H₂(s) in BoundedFunctions A ) ; :: thesis: verum

end;

consider x being Function of [.a,b.],(BoundedFunctions A) such that
A19: for s being object st s in [.a,b.] holds
( ( S₁[s] implies x . s = H₁(s) ) & ( not S₁[s] implies x . s = H₂(s) ) ) from FUNCT_2:sch 5(A3);
reconsider x = x as Function of A,(BoundedFunctions A) by A2;
take x ; :: thesis: for s being Real st s in [.a,b.] holds
( ( s = a implies x . s = [.a,b.] --> 0 ) & ( s <> a implies x . s = ([.a,s.] --> 1) +* (].s,b.] --> 0) ) )
for s being Real st s in [.a,b.] holds
( ( s = a implies x . s = [.a,b.] --> 0 ) & ( s <> a implies x . s = ([.a,s.] --> 1) +* (].s,b.] --> 0) ) )

proof

let s be Real; :: thesis: ( s in [.a,b.] implies ( ( s = a implies x . s = [.a,b.] --> 0 ) & ( s <> a implies x . s = ([.a,s.] --> 1) +* (].s,b.] --> 0) ) ) )
assume A20: s in [.a,b.] ; :: thesis: ( ( s = a implies x . s = [.a,b.] --> 0 ) & ( s <> a implies x . s = ([.a,s.] --> 1) +* (].s,b.] --> 0) ) )
In (s,REAL) = s ;
hence ( ( s = a implies x . s = [.a,b.] --> 0 ) & ( s <> a implies x . s = ([.a,s.] --> 1) +* (].s,b.] --> 0) ) ) by A19, A20; :: thesis: verum

end;

hence for s being Real st s in [.a,b.] holds
( ( s = a implies x . s = [.a,b.] --> 0 ) & ( s <> a implies x . s = ([.a,s.] --> 1) +* (].s,b.] --> 0) ) ) ; :: thesis: verum