A1:
for x being set holds

( x in REAL n iff x is Function of (Seg n),REAL )

( 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

( x in REAL n iff x is Function of (Seg n),REAL )

proof

let X be FinSequenceSet of REAL ; :: thesis: ( X = REAL n iff for x being object holds
let x be set ; :: thesis: ( x in REAL n iff x is Function of (Seg n),REAL )

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;hereby :: thesis: ( x is Function of (Seg n),REAL implies x in REAL n )

assume
x is Function of (Seg n),REAL
; :: thesis: x in REAL nassume
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;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

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

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

hence
X = REAL n
by TARSKI:2; :: thesis: verum( 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;( 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