let f be complex-valued Function; :: thesis: 1 (#) f = f

A1: now :: thesis: for c being object st c in dom (1 (#) f) holds
(1 (#) f) . c = f . c

let c be object ; :: thesis: ( c in dom (1 (#) f) implies (1 (#) f) . c = f . c )
assume c in dom (1 (#) f) ; :: thesis: (1 (#) f) . c = f . c
hence (1 (#) f) . c = 1 * (f . c) by VALUED_1:def 5
.= f . c ;
:: thesis: verum

end;

dom (1 (#) f) = dom f by VALUED_1:def 5;
hence 1 (#) f = f by A1, FUNCT_1:2; :: thesis: verum