let f be Real_Sequence; :: thesis: ( f = Re c iff for n being Element of NAT holds f . n = Re (c . n) )
a0: dom (Re c) = dom c by Def1a;
a2: dom c = NAT by FUNCT_2:def 1;
a3: dom f = NAT by FUNCT_2:def 1;
hence ( f = Re c implies for n being Element of NAT holds f . n = Re (c . n) ) by Def1a; :: thesis: ( ( for n being Element of NAT holds f . n = Re (c . n) ) implies f = Re c )
assume a4: for n being Element of NAT holds f . n = Re (c . n) ; :: thesis: f = Re c

now

let x be set ; :: thesis: ( x in dom f implies f . x = (Re c) . x )
assume a5: x in dom f ; :: thesis: f . x = (Re c) . x
hence f . x = Re (c . x) by a3, a4
.= (Re c) . x by a0, a2, a3, a5, Def1a ;
:: thesis: verum

end;

hence f = Re c by a0, a2, a3, FUNCT_1:9; :: thesis: verum