A1: ( rng f c= OddNAT & rng g c= OddNAT ) by Def1;
rng (f ^ g) = (rng f) \/ (rng g) by FINSEQ_1:31;
hence f ^ g is odd-valued by A1, XBOOLE_1:8; :: thesis: verum