A1: for x being set holds
( x in REAL n iff x is Function of Seg n, REAL )

proof

let x be set ; :: thesis: ( x in REAL n iff x is Function of Seg n, REAL )

hereby :: thesis: ( x is Function of Seg n, REAL implies x in REAL n )

assume x in REAL n ; :: thesis: x is Function of Seg n, REAL
then x in n -tuples_on REAL by EUCLID:def 1;
then x in Funcs (Seg n),REAL by FINSEQ_2:111;
hence x is Function of Seg n, REAL by FUNCT_2:121; :: thesis: verum

end;

assume x is Function of Seg n, REAL ; :: thesis: x in REAL n
then x in Funcs (Seg n),REAL by FUNCT_2:11;
then x in n -tuples_on REAL by FINSEQ_2:111;
hence x in REAL n by EUCLID:def 1; :: thesis: verum

end;

let X be FinSequence-DOMAIN of ; :: thesis: ( X = REAL n iff for x being set holds
( x in X iff x is Function of Seg n, REAL ) )
thus ( X = REAL n implies for x being set holds
( x in X iff x is Function of Seg n, REAL ) ) by A1; :: thesis: ( ( for x being set holds
( x in X iff x is Function of Seg n, REAL ) ) implies X = REAL n )
assume A2: for x being set holds
( x in X iff x is Function of Seg n, REAL ) ; :: thesis: X = REAL n

now

let x be set ; :: thesis: ( x in X iff x in REAL n )
( x in X iff x is Function of Seg n, REAL ) by A2;
hence ( x in X iff x in REAL n ) by A1; :: thesis: verum

end;

hence X = REAL n by TARSKI:2; :: thesis: verum