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

proof

let t be Real; :: thesis: ( t in ].r,s.[ implies 1 |-> t in OpenHyperInterval (<*r*>,<*s*>) )
assume A2: t in ].r,s.[ ; :: thesis: 1 |-> t in OpenHyperInterval (<*r*>,<*s*>)
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).[ ) )

proof

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

proof

let i be Nat; :: thesis: ( i in Seg 1 implies t1 . i in ].(<*r*> . i),(<*s*> . i).[ )
assume A3: i in Seg 1 ; :: thesis: t1 . i in ].(<*r*> . i),(<*s*> . i).[
then A4: i = 1 by FINSEQ_1:2, TARSKI:def 1;

now :: thesis: ( t1 . i = t & <*r*> . i = r & <*s*> . i = s )

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

end;

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

end;

end;

hence 1 |-> t in OpenHyperInterval (<*r*>,<*s*>) by Def4; :: thesis: verum

end;

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

proof

let x be Real; :: thesis: ( 1 |-> x in OpenHyperInterval (<*r*>,<*s*>) implies x in ].r,s.[ )
assume 1 |-> x in OpenHyperInterval (<*r*>,<*s*>) ; :: thesis: x in ].r,s.[
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 Def4;
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 ) ;
hence x in ].r,s.[ by A6, A7, A8; :: thesis: verum

end;

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