A1: rng (F ^ G) = (rng F) \/ (rng G) by FINSEQ_1:31;
now :: thesis: for y being set st y in rng (F ^ G) holds
y is FinSequence
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 Th25; :: thesis: verum
end;
hence F ^ G is FinSequence-yielding by Th25; :: thesis: verum