let X be set ; :: thesis: for Y being non empty set
for p being FinSequence of X
for f being Function of X,Y holds f * p is FinSequence of Y
let Y be non empty set ; :: thesis: for p being FinSequence of X
for f being Function of X,Y holds f * p is FinSequence of Y
let p be FinSequence of X; :: thesis: for f being Function of X,Y holds f * p is FinSequence of Y
let f be Function of X,Y; :: thesis: f * p is FinSequence of Y
A1: rng p c= X ;
dom f = X by FUNCT_2:def 1;
then dom (f * p) = dom p by A1, RELAT_1:27;
then A2: f * p is FinSequence by Lm1;
rng (f * p) c= Y ;
hence f * p is FinSequence of Y by A2, FINSEQ_1:def 4; :: thesis: verum