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

now

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 Th22; :: thesis: verum

end;

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