rng f c= B
by FINSEQ_1:def 4;

then rng f c= A by XBOOLE_1:1;

then rng f c= dom g by FUNCT_2:def 1;

hence g * f is FinSequence-like by FINSEQ_1:16; :: thesis: verum

then rng f c= A by XBOOLE_1:1;

then rng f c= dom g by FUNCT_2:def 1;

hence g * f is FinSequence-like by FINSEQ_1:16; :: thesis: verum