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
( rng p c= X & dom f = X ) by FUNCT_2:def 1;
then ( dom (f * p) = dom p & rng f c= Y & rng (f * p) c= rng f ) by RELAT_1:45, RELAT_1:46;
then ( f * p is FinSequence & rng (f * p) c= Y ) by Lm1;
hence f * p is FinSequence of Y by FINSEQ_1:def 4; :: thesis: verum