let c be Complex; :: thesis: 0 (#) (NAT --> c) = NAT --> 0
A1: dom (0 (#) (NAT --> c)) = dom (NAT --> c) by VALUED_1:def 5
.= dom (NAT --> 0) ;
for k being object st k in dom (NAT --> 0) holds
(NAT --> 0) . k = (0 (#) (NAT --> c)) . k

proof

let k be object ; :: thesis: ( k in dom (NAT --> 0) implies (NAT --> 0) . k = (0 (#) (NAT --> c)) . k )
assume B1: k in dom (NAT --> 0) ; :: thesis: (NAT --> 0) . k = (0 (#) (NAT --> c)) . k
reconsider k = k as Nat by B1;
(NAT --> 0) . k = 0 * ((NAT --> c) . k)
.= (0 (#) (NAT --> c)) . k by A1, B1, VALUED_1:def 5 ;
hence (NAT --> 0) . k = (0 (#) (NAT --> c)) . k ; :: thesis: verum

end;

hence 0 (#) (NAT --> c) = NAT --> 0 by A1; :: thesis: verum