let A, D be set ; :: thesis: for p being FinSequence of A
for f being Function of A,D holds f * p is FinSequence of D
let p be FinSequence of A; :: thesis: for f being Function of A,D holds f * p is FinSequence of D
let f be Function of A,D; :: thesis: f * p is FinSequence of D

per cases ( D = {} or D <> {} ) ;

suppose D = {} ; :: thesis: f * p is FinSequence of D

then f * p = <*> D ;
hence f * p is FinSequence of D ; :: thesis: verum

end;

suppose A1: D <> {} ; :: thesis: f * p is FinSequence of D

A2: rng p c= A by RELAT_1:def 19;
A3: rng (f * p) c= D by RELAT_1:def 19;
dom f = A by A1, FUNCT_2:def 1;
then f * p is FinSequence by A2, FINSEQ_1:16;
hence f * p is FinSequence of D by A3, FINSEQ_1:def 4; :: thesis: verum

end;

end;