let r, s be Real; :: thesis:
set a1 = <*r*>;
set b1 = <*s*>;
A1: for x being Real st x in ].r,s.] holds
1 |-> x in LeftOpenHyperInterval (<*r*>,<*s*>)

let t be Real; :: thesis:
assume A2: t in ].r,s.] ; :: thesis:
reconsider t1 = 1 |-> t as Element of REAL 1 ;
ex y being Element of REAL 1 st
( t1 = y & ( for i being Nat st i in Seg 1 holds
y . i in ].(<*r*> . i),(<*s*> . i).] ) )

take t1 ; :: thesis:
thus t1 = t1 ; :: thesis:
thus for i being Nat st i in Seg 1 holds
t1 . i in ].(<*r*> . i),(<*s*> . i).] :: thesis:

let i be Nat; :: thesis:
assume A3: i in Seg 1 ; :: thesis:
then A4: i = 1 by FINSEQ_1:2, TARSKI:def 1;

t1 . 1 = ((Seg 1) --> t) . 1 by FINSEQ_2:def 2;
hence t1 . i = t by A3, A4, FUNCOP_1:7; :: thesis:
thus ( <*r*> . i = r & <*s*> . i = s ) by A4, FINSEQ_1:def 8; :: thesis:

end;

hence t1 . i in ].(<*r*> . i),(<*s*> . i).] by A2; :: thesis:

end;

end;

hence 1 |-> t in LeftOpenHyperInterval (<*r*>,<*s*>) by Def5; :: thesis:

end;

for x being Real st 1 |-> x in LeftOpenHyperInterval (<*r*>,<*s*>) holds
x in ].r,s.]

let x be Real; :: thesis:
assume 1 |-> x in LeftOpenHyperInterval (<*r*>,<*s*>) ; :: thesis:
then consider y being Element of REAL 1 such that
A5: 1 |-> x = y and
A6: for i being Nat st i in Seg 1 holds
y . i in ].(<*r*> . i),(<*s*> . i).] by Def5;
A7: 1 in Seg 1 ;
( y = (Seg 1) --> x & 1 in Seg 1 ) by A5, FINSEQ_2:def 2;
then A8: y . 1 = x by FUNCOP_1:7;
( <*r*> . 1 = r & <*s*> . 1 = s ) by FINSEQ_1:def 8;
hence x in ].r,s.] by A6, A7, A8; :: thesis:

end;

hence for x being Real holds
( x in ].r,s.] iff 1 |-> x in LeftOpenHyperInterval (<*r*>,<*s*>) ) by A1; :: thesis: