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

( 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