reconsider zeroseq = NAT --> 0 as Real_Sequence by FUNCOP_1:57;
zeroseq in the_set_of_RealSequences by Def1;
then A1: seq_id zeroseq = zeroseq by Def2;
reconsider zeroseq = zeroseq as Element of the_set_of_RealSequences by Def1;
take zeroseq ; :: thesis: for n being Element of NAT holds (seq_id zeroseq) . n = 0
let n be Nat; :: thesis: ( n is Element of REAL & n is Element of NAT implies (seq_id zeroseq) . n = 0 )
thus ( n is Element of REAL & n is Element of NAT implies (seq_id zeroseq) . n = 0 ) by A1, FUNCOP_1:13; :: thesis: verum