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

now

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

end;

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