let S be non empty set ; :: thesis:
let p, q be FinSequence of S; :: thesis:
assume AS: ( p is 48 -element & q is 8 -element ) ; :: thesis:
set r = p ^ q;
L1: ( len p = 48 & len q = 8 ) by AS, CARD_1:def 7;
len (p ^ q) = (len p) + (len q) by FINSEQ_1:22
.= 56 by L1 ;
hence p ^ q is 56 -element by CARD_1:def 7; :: thesis:
L50: dom p = Seg 48 by L1, FINSEQ_1:def 3;
L51: dom q = Seg 8 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 & 33 in dom p & 34 in dom p & 35 in dom p & 36 in dom p & 37 in dom p & 38 in dom p & 39 in dom p & 40 in dom p & 41 in dom p & 42 in dom p & 43 in dom p & 44 in dom p & 45 in dom p & 46 in dom p & 47 in dom p & 48 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 & (p ^ q) . 33 = p . 33 & (p ^ q) . 34 = p . 34 & (p ^ q) . 35 = p . 35 & (p ^ q) . 36 = p . 36 & (p ^ q) . 37 = p . 37 & (p ^ q) . 38 = p . 38 & (p ^ q) . 39 = p . 39 & (p ^ q) . 40 = p . 40 & (p ^ q) . 41 = p . 41 & (p ^ q) . 42 = p . 42 & (p ^ q) . 43 = p . 43 & (p ^ q) . 44 = p . 44 & (p ^ q) . 45 = p . 45 & (p ^ q) . 46 = p . 46 & (p ^ q) . 47 = p . 47 & (p ^ q) . 48 = p . 48 ) 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 ) by L51;
then ( (p ^ q) . (48 + 1) = q . 1 & (p ^ q) . (48 + 2) = q . 2 & (p ^ q) . (48 + 3) = q . 3 & (p ^ q) . (48 + 4) = q . 4 & (p ^ q) . (48 + 5) = q . 5 & (p ^ q) . (48 + 6) = q . 6 & (p ^ q) . (48 + 7) = q . 7 & (p ^ q) . (48 + 8) = q . 8 ) by L1, FINSEQ_1:def 7;
hence ( (p ^ q) . 49 = q . 1 & (p ^ q) . 50 = q . 2 & (p ^ q) . 51 = q . 3 & (p ^ q) . 52 = q . 4 & (p ^ q) . 53 = q . 5 & (p ^ q) . 54 = q . 6 & (p ^ q) . 55 = q . 7 & (p ^ q) . 56 = q . 8 ) ; :: thesis: