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 )
consider n being Nat such that
A1: dom f1 = Seg n by FINSEQ_1:def 2;
assume rng f1 c= dom f2 ; :: thesis: f2 * f1 is FinSequence of X
then dom (f2 * f1) = Seg n by A1, RELAT_1:27;
then A2: f2 * f1 is FinSequence by FINSEQ_1:def 2;
rng (f2 * f1) c= X ;
hence f2 * f1 is FinSequence of X by A2, FINSEQ_1:def 4; :: thesis: verum