(Funcs) (A,B) is V2() by A1, Th18;
then not {} in rng ((Funcs) (A,B)) by PBOOLE:137;
hence product ((Funcs) (A,B)) is non empty set by CARD_3:26; :: thesis: verum