{ (Base_FinSeq n,i) where i is Element of NAT : ( 1 <= i & i <= n ) } c= REAL n

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (Base_FinSeq n,i) where i is Element of NAT : ( 1 <= i & i <= n ) } or x in REAL n )
assume x in { (Base_FinSeq n,i) where i is Element of NAT : ( 1 <= i & i <= n ) } ; :: thesis: x in REAL n
then ex i being Element of NAT st
( x = Base_FinSeq n,i & 1 <= i & i <= n ) ;
hence x in REAL n ; :: thesis: verum

end;

hence { (Base_FinSeq n,i) where i is Element of NAT : ( 1 <= i & i <= n ) } is Subset of (REAL n) ; :: thesis: verum