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

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