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 ) 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