let a, b, x be Real; ( a <= x & x <= b implies <*x*> in product <*[.a,b.]*> )
assume A1:
( a <= x & x <= b )
; <*x*> in product <*[.a,b.]*>
reconsider P = <*x*> as Point of (Euclid 1) by Th7;
set f = <*[.a,b.]*>;
A2:
dom <*[.a,b.]*> = Seg 1
by FINSEQ_1:def 8;
ex g being Function st
( g = P & dom g = dom <*[.a,b.]*> & ( for y being object st y in dom <*[.a,b.]*> holds
g . y in <*[.a,b.]*> . y ) )
proof
reconsider g =
P as
Function ;
now ex g being Function st
( g = P & dom g = dom <*[.a,b.]*> & ( for y being object st y in dom <*[.a,b.]*> holds
g . y in <*[.a,b.]*> . y ) )take g =
g;
( g = P & dom g = dom <*[.a,b.]*> & ( for y being object st y in dom <*[.a,b.]*> holds
g . y in <*[.a,b.]*> . y ) )thus
g = P
;
( dom g = dom <*[.a,b.]*> & ( for y being object st y in dom <*[.a,b.]*> holds
g . y in <*[.a,b.]*> . y ) )thus
dom g = dom <*[.a,b.]*>
by A2, FINSEQ_1:def 8;
for y being object st y in dom <*[.a,b.]*> holds
g . y in <*[.a,b.]*> . yhereby verum
let y be
object ;
( y in dom <*[.a,b.]*> implies g . y in <*[.a,b.]*> . y )assume
y in dom <*[.a,b.]*>
;
g . y in <*[.a,b.]*> . ythen
y in {1}
by FINSEQ_1:def 8, FINSEQ_1:2;
then A3:
y = 1
by TARSKI:def 1;
(
g . 1
= x &
<*[.a,b.]*> . 1
= [.a,b.] )
by FINSEQ_1:def 8;
hence
g . y in <*[.a,b.]*> . y
by A3, A1, XXREAL_1:1;
verum
end; end;
hence
ex
g being
Function st
(
g = P &
dom g = dom <*[.a,b.]*> & ( for
y being
object st
y in dom <*[.a,b.]*> holds
g . y in <*[.a,b.]*> . y ) )
;
verum
end;
hence
<*x*> in product <*[.a,b.]*>
by CARD_3:def 5; verum