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 Cardinal

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

end;

hence F ^ G is Cardinal-yielding by Th21; :: thesis: verum