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:93;
hence x is Function of (Seg n),REAL by FUNCT_2:66; :: 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:8;
then x in n -tuples_on REAL by FINSEQ_2:93;
hence x in REAL n by EUCLID:def 1; :: thesis: verum

end;

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

now :: thesis: for x being object holds
( x in X iff x in REAL n )

let x be object ; :: 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