let S be non empty set ; :: thesis:
let p, q be FinSequence of S; :: thesis:
assume AS: ( p is 32 -element & q is 32 -element ) ; :: thesis:
set r = p ^ q;
L1: ( len p = 32 & len q = 32 ) by AS, CARD_1:def 7;
len (p ^ q) = (len p) + (len q) by FINSEQ_1:22
.= 64 by L1 ;
hence p ^ q is 64 -element by CARD_1:def 7; :: thesis:
L50: dom p = Seg 32 by L1, FINSEQ_1:def 3;
L51: dom q = Seg 32 by L1, FINSEQ_1:def 3;
( 1 in dom p & 2 in dom p & 3 in dom p & 4 in dom p & 5 in dom p & 6 in dom p & 7 in dom p & 8 in dom p & 9 in dom p & 10 in dom p & 11 in dom p & 12 in dom p & 13 in dom p & 14 in dom p & 15 in dom p & 16 in dom p & 17 in dom p & 18 in dom p & 19 in dom p & 20 in dom p & 21 in dom p & 22 in dom p & 23 in dom p & 24 in dom p & 25 in dom p & 26 in dom p & 27 in dom p & 28 in dom p & 29 in dom p & 30 in dom p & 31 in dom p & 32 in dom p ) by L50;
hence ( (p ^ q) . 1 = p . 1 & (p ^ q) . 2 = p . 2 & (p ^ q) . 3 = p . 3 & (p ^ q) . 4 = p . 4 & (p ^ q) . 5 = p . 5 & (p ^ q) . 6 = p . 6 & (p ^ q) . 7 = p . 7 & (p ^ q) . 8 = p . 8 & (p ^ q) . 9 = p . 9 & (p ^ q) . 10 = p . 10 & (p ^ q) . 11 = p . 11 & (p ^ q) . 12 = p . 12 & (p ^ q) . 13 = p . 13 & (p ^ q) . 14 = p . 14 & (p ^ q) . 15 = p . 15 & (p ^ q) . 16 = p . 16 & (p ^ q) . 17 = p . 17 & (p ^ q) . 18 = p . 18 & (p ^ q) . 19 = p . 19 & (p ^ q) . 20 = p . 20 & (p ^ q) . 21 = p . 21 & (p ^ q) . 22 = p . 22 & (p ^ q) . 23 = p . 23 & (p ^ q) . 24 = p . 24 & (p ^ q) . 25 = p . 25 & (p ^ q) . 26 = p . 26 & (p ^ q) . 27 = p . 27 & (p ^ q) . 28 = p . 28 & (p ^ q) . 29 = p . 29 & (p ^ q) . 30 = p . 30 & (p ^ q) . 31 = p . 31 & (p ^ q) . 32 = p . 32 ) by FINSEQ_1:def 7; :: thesis:
( 1 in dom q & 2 in dom q & 3 in dom q & 4 in dom q & 5 in dom q & 6 in dom q & 7 in dom q & 8 in dom q & 9 in dom q & 10 in dom q & 11 in dom q & 12 in dom q & 13 in dom q & 14 in dom q & 15 in dom q & 16 in dom q & 17 in dom q & 18 in dom q & 19 in dom q & 20 in dom q & 21 in dom q & 22 in dom q & 23 in dom q & 24 in dom q & 25 in dom q & 26 in dom q & 27 in dom q & 28 in dom q & 29 in dom q & 30 in dom q & 31 in dom q & 32 in dom q ) by L51;
then ( (p ^ q) . (32 + 1) = q . 1 & (p ^ q) . (32 + 2) = q . 2 & (p ^ q) . (32 + 3) = q . 3 & (p ^ q) . (32 + 4) = q . 4 & (p ^ q) . (32 + 5) = q . 5 & (p ^ q) . (32 + 6) = q . 6 & (p ^ q) . (32 + 7) = q . 7 & (p ^ q) . (32 + 8) = q . 8 & (p ^ q) . (32 + 9) = q . 9 & (p ^ q) . (32 + 10) = q . 10 & (p ^ q) . (32 + 11) = q . 11 & (p ^ q) . (32 + 12) = q . 12 & (p ^ q) . (32 + 13) = q . 13 & (p ^ q) . (32 + 14) = q . 14 & (p ^ q) . (32 + 15) = q . 15 & (p ^ q) . (32 + 16) = q . 16 & (p ^ q) . (32 + 17) = q . 17 & (p ^ q) . (32 + 18) = q . 18 & (p ^ q) . (32 + 19) = q . 19 & (p ^ q) . (32 + 20) = q . 20 & (p ^ q) . (32 + 21) = q . 21 & (p ^ q) . (32 + 22) = q . 22 & (p ^ q) . (32 + 23) = q . 23 & (p ^ q) . (32 + 24) = q . 24 & (p ^ q) . (32 + 25) = q . 25 & (p ^ q) . (32 + 26) = q . 26 & (p ^ q) . (32 + 27) = q . 27 & (p ^ q) . (32 + 28) = q . 28 & (p ^ q) . (32 + 29) = q . 29 & (p ^ q) . (32 + 30) = q . 30 & (p ^ q) . (32 + 31) = q . 31 & (p ^ q) . (32 + 32) = q . 32 ) by L1, FINSEQ_1:def 7;
hence ( (p ^ q) . 33 = q . 1 & (p ^ q) . 34 = q . 2 & (p ^ q) . 35 = q . 3 & (p ^ q) . 36 = q . 4 & (p ^ q) . 37 = q . 5 & (p ^ q) . 38 = q . 6 & (p ^ q) . 39 = q . 7 & (p ^ q) . 40 = q . 8 & (p ^ q) . 41 = q . 9 & (p ^ q) . 42 = q . 10 & (p ^ q) . 43 = q . 11 & (p ^ q) . 44 = q . 12 & (p ^ q) . 45 = q . 13 & (p ^ q) . 46 = q . 14 & (p ^ q) . 47 = q . 15 & (p ^ q) . 48 = q . 16 & (p ^ q) . 49 = q . 17 & (p ^ q) . 50 = q . 18 & (p ^ q) . 51 = q . 19 & (p ^ q) . 52 = q . 20 & (p ^ q) . 53 = q . 21 & (p ^ q) . 54 = q . 22 & (p ^ q) . 55 = q . 23 & (p ^ q) . 56 = q . 24 & (p ^ q) . 57 = q . 25 & (p ^ q) . 58 = q . 26 & (p ^ q) . 59 = q . 27 & (p ^ q) . 60 = q . 28 & (p ^ q) . 61 = q . 29 & (p ^ q) . 62 = q . 30 & (p ^ q) . 63 = q . 31 & (p ^ q) . 64 = q . 32 ) ; :: thesis: