A1: rng (F ^ G) = (rng F) \/ (rng G) by FINSEQ_1:44;

now

let y be set ; :: thesis: ( y in rng (F ^ G) implies y is FinSequence )
assume y in rng (F ^ G) ; :: thesis: y is FinSequence
then ( y in rng F or y in rng G ) by A1, XBOOLE_0:def 3;
hence y is FinSequence by Th14; :: thesis: verum

end;

hence F ^ G is FinSequence-yielding by Th14; :: thesis: verum