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 S = NAT & rng S c= the carrier of X ) by FUNCT_2:def 1;
A2: dom f = the carrier of (TopSpaceMetr X) by FUNCT_2:def 1
.= the carrier of X by TOPMETR:16 ;
the carrier of Y = the carrier of (TopSpaceMetr Y) by TOPMETR:16;
then ( dom (f * S) = NAT & rng (f * S) c= the carrier of Y ) by A1, A2, RELAT_1:46;
hence f * S is sequence of Y by FUNCT_2:def 1, RELSET_1:11; :: thesis: verum