let S be non empty set ; :: thesis:
let p, q be FinSequence of S; :: thesis:
assume AS: ( p is 16 -element & q is 16 -element ) ; :: thesis:
set r = p ^ q;
L1: ( len p = 16 & len q = 16 ) by AS, CARD_1:def 7;
len (p ^ q) = (len p) + (len q) by FINSEQ_1:22
.= 32 by L1 ;
hence p ^ q is 32 -element by CARD_1:def 7; :: thesis:
L50: dom p = Seg 16 by L1, FINSEQ_1:def 3;
L51: dom q = Seg 16 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 ) 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 ) 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 ) by L51;
then ( (p ^ q) . (16 + 1) = q . 1 & (p ^ q) . (16 + 2) = q . 2 & (p ^ q) . (16 + 3) = q . 3 & (p ^ q) . (16 + 4) = q . 4 & (p ^ q) . (16 + 5) = q . 5 & (p ^ q) . (16 + 6) = q . 6 & (p ^ q) . (16 + 7) = q . 7 & (p ^ q) . (16 + 8) = q . 8 & (p ^ q) . (16 + 9) = q . 9 & (p ^ q) . (16 + 10) = q . 10 & (p ^ q) . (16 + 11) = q . 11 & (p ^ q) . (16 + 12) = q . 12 & (p ^ q) . (16 + 13) = q . 13 & (p ^ q) . (16 + 14) = q . 14 & (p ^ q) . (16 + 15) = q . 15 & (p ^ q) . (16 + 16) = q . 16 ) by L1, FINSEQ_1:def 7;
hence ( (p ^ q) . 17 = q . 1 & (p ^ q) . 18 = q . 2 & (p ^ q) . 19 = q . 3 & (p ^ q) . 20 = q . 4 & (p ^ q) . 21 = q . 5 & (p ^ q) . 22 = q . 6 & (p ^ q) . 23 = q . 7 & (p ^ q) . 24 = q . 8 & (p ^ q) . 25 = q . 9 & (p ^ q) . 26 = q . 10 & (p ^ q) . 27 = q . 11 & (p ^ q) . 28 = q . 12 & (p ^ q) . 29 = q . 13 & (p ^ q) . 30 = q . 14 & (p ^ q) . 31 = q . 15 & (p ^ q) . 32 = q . 16 ) ; :: thesis: