let n be Nat; :: thesis: for s1 being sequence of (Euclid n)
for s2 being sequence of (REAL-NS n) holds
( s1 is sequence of (REAL-NS n) & s2 is sequence of (Euclid n) )
let s1 be sequence of (Euclid n); :: thesis: for s2 being sequence of (REAL-NS n) holds
( s1 is sequence of (REAL-NS n) & s2 is sequence of (Euclid n) )
let s2 be sequence of (REAL-NS n); :: thesis: ( s1 is sequence of (REAL-NS n) & s2 is sequence of (Euclid n) )
thus s1 is sequence of (REAL-NS n) :: thesis: s2 is sequence of (Euclid n)

proof

s1 is sequence of the carrier of (TOP-REAL n) by EUCLID:67;
then s1 is sequence of (REAL n) by EUCLID:22;
hence s1 is sequence of (REAL-NS n) by REAL_NS1:def 4; :: thesis: verum

end;

thus s2 is sequence of (Euclid n) :: thesis: verum

proof

s2 is sequence of (REAL n) by REAL_NS1:def 4;
then s2 is sequence of (TOP-REAL n) by EUCLID:22;
hence s2 is sequence of (Euclid n) by EUCLID:67; :: thesis: verum

end;