len (x ^ y) = 56 by CARD_1:def 7;
hence x ^ y is Element of 56 -tuples_on BOOLEAN by FINSEQ_2:92; :: thesis: verum