let f be Real_Sequence; :: thesis: ( f = Re c iff for n being Element of NAT holds f . n = Re (c . n) )
A1: dom (Re c) = dom c by Def3;
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 Def3; :: 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 A1, A2, A3, A5, Def3 ;
:: thesis: verum

end;

hence f = Re c by A1, A2, A3, FUNCT_1:2; :: thesis: verum