let X be set ; :: thesis: for f1 being FinSequence of NAT
for f2 being FinSequence of X st rng f1 c= dom f2 holds
f2 * f1 is FinSequence of X
let f1 be FinSequence of NAT ; :: thesis: for f2 being FinSequence of X st rng f1 c= dom f2 holds
f2 * f1 is FinSequence of X
let f2 be FinSequence of X; :: thesis: ( rng f1 c= dom f2 implies f2 * f1 is FinSequence of X )
assume A1: rng f1 c= dom f2 ; :: thesis: f2 * f1 is FinSequence of X
consider n being natural number such that
A2: dom f1 = Seg n by FINSEQ_1:def 2;
dom (f2 * f1) = Seg n by A1, A2, RELAT_1:46;
then A3: f2 * f1 is FinSequence by FINSEQ_1:def 2;
rng (f2 * f1) c= X ;
hence f2 * f1 is FinSequence of X by A3, FINSEQ_1:def 4; :: thesis: verum