let a, b, x be Real; :: thesis: ( a <= x & x <= b implies <*x*> in product <*[.a,b.]*> )
assume A1: ( a <= x & x <= b ) ; :: thesis: <*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 :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: for y being object st y in dom <*[.a,b.]*> holds
g . y in <*[.a,b.]*> . y

hereby :: thesis: verum

let y be object ; :: thesis: ( y in dom <*[.a,b.]*> implies g . y in <*[.a,b.]*> . y )
assume y in dom <*[.a,b.]*> ; :: thesis: g . y in <*[.a,b.]*> . y
then 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; :: thesis: 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 ) ) ; :: thesis: verum

end;

hence <*x*> in product <*[.a,b.]*> by CARD_3:def 5; :: thesis: verum