let X, Y be non empty MetrSpace; :: thesis: for f being Function of (TopSpaceMetr X),(TopSpaceMetr Y)
for S being sequence of X holds f * S is sequence of Y
let f be Function of (TopSpaceMetr X),(TopSpaceMetr Y); :: thesis: for S being sequence of X holds f * S is sequence of Y
let S be sequence of X; :: thesis: f * S is sequence of Y
A1: dom f = the carrier of (TopSpaceMetr X) by FUNCT_2:def 1
.= the carrier of X by TOPMETR:12 ;
( dom S = NAT & rng S c= the carrier of X ) by FUNCT_2:def 1;
then dom (f * S) = NAT by A1, RELAT_1:27;
hence f * S is sequence of Y by FUNCT_2:def 1, TOPMETR:12; :: thesis: verum