let f be Real_Sequence; :: thesis: ( f = Im c iff for n being Nat holds f . n = Im (c . n) )
A6: dom (Im c) = dom c by Def4;
A7: dom c = NAT by FUNCT_2:def 1;
A8: dom f = NAT by FUNCT_2:def 1;
thus ( f = Im c implies for n being Nat holds f . n = Im (c . n) ) by A6, A7, ORDINAL1:def 12, Def4; :: thesis: ( ( for n being Nat holds f . n = Im (c . n) ) implies f = Im c )
assume A9: for n being Nat holds f . n = Im (c . n) ; :: thesis: f = Im c
now :: thesis: for x being object st x in dom f holds
f . x = (Im c) . x
let x be object ; :: thesis: ( x in dom f implies f . x = (Im c) . x )
assume A10: x in dom f ; :: thesis: f . x = (Im c) . x
hence f . x = Im (c . x) by A9
.= (Im c) . x by A6, A7, A8, A10, Def4 ;
:: thesis: verum
end;
hence f = Im c by A6, A7, A8, FUNCT_1:2; :: thesis: verum