let f be Real_Sequence; :: thesis: ( f = Re c iff for n being 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;
thus ( f = Re c implies for n being Nat holds f . n = Re (c . n) ) by A1, A2, Def3, ORDINAL1:def 12; :: thesis: ( ( for n being Nat holds f . n = Re (c . n) ) implies f = Re c )
assume A4: for n being Nat holds f . n = Re (c . n) ; :: thesis: f = Re c

now :: thesis: for x being object st x in dom f holds
f . x = (Re c) . x

let x be object ; :: 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 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