let n be Nat; :: thesis: for f being set holds
( f is sequence of (REAL-NS n) iff f is sequence of (REAL-US n) )
let f be set ; :: thesis: ( f is sequence of (REAL-NS n) iff f is sequence of (REAL-US n) )
the carrier of (REAL-NS n) = REAL n by Def4
.= the carrier of (REAL-US n) by Def6 ;
hence ( f is sequence of (REAL-NS n) iff f is sequence of (REAL-US n) ) ; :: thesis: verum