thus ( f is complex-functions-valued implies for x being object st x in dom f holds
f . x is complex-valued Function ) :: thesis: ( ( for x being object st x in dom f holds
f . x is complex-valued Function ) implies f is complex-functions-valued )
proof
assume A1: rng f is complex-functions-membered ; :: according to VALUED_2:def 20 :: thesis: for x being object st x in dom f holds
f . x is complex-valued Function

let x be object ; :: thesis: ( x in dom f implies f . x is complex-valued Function )
assume x in dom f ; :: thesis:
then f . x in rng f by FUNCT_1:def 3;
hence f . x is complex-valued Function by A1; :: thesis: verum
end;
assume A2: for x being object st x in dom f holds
f . x is complex-valued Function ; :: thesis:
let y be object ; :: according to VALUED_2:def 2,VALUED_2:def 20 :: thesis: ( y in rng f implies y is complex-valued Function )
assume y in rng f ; :: thesis:
then ex x being object st
( x in dom f & f . x = y ) by FUNCT_1:def 3;
hence y is complex-valued Function by A2; :: thesis: verum