let S be non empty set ; for p, q being FinSequence of S st p is 8 -element & q is 8 -element holds
( p ^ q is 16 -element & (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 = q . 1 & (p ^ q) . 10 = q . 2 & (p ^ q) . 11 = q . 3 & (p ^ q) . 12 = q . 4 & (p ^ q) . 13 = q . 5 & (p ^ q) . 14 = q . 6 & (p ^ q) . 15 = q . 7 & (p ^ q) . 16 = q . 8 )
let p, q be FinSequence of S; ( p is 8 -element & q is 8 -element implies ( p ^ q is 16 -element & (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 = q . 1 & (p ^ q) . 10 = q . 2 & (p ^ q) . 11 = q . 3 & (p ^ q) . 12 = q . 4 & (p ^ q) . 13 = q . 5 & (p ^ q) . 14 = q . 6 & (p ^ q) . 15 = q . 7 & (p ^ q) . 16 = q . 8 ) )
assume AS:
( p is 8 -element & q is 8 -element )
; ( p ^ q is 16 -element & (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 = q . 1 & (p ^ q) . 10 = q . 2 & (p ^ q) . 11 = q . 3 & (p ^ q) . 12 = q . 4 & (p ^ q) . 13 = q . 5 & (p ^ q) . 14 = q . 6 & (p ^ q) . 15 = q . 7 & (p ^ q) . 16 = q . 8 )
set r = p ^ q;
L1:
( len p = 8 & len q = 8 )
by AS, CARD_1:def 7;
len (p ^ q) =
(len p) + (len q)
by FINSEQ_1:22
.=
16
by L1
;
hence
p ^ q is 16 -element
by CARD_1:def 7; ( (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 = q . 1 & (p ^ q) . 10 = q . 2 & (p ^ q) . 11 = q . 3 & (p ^ q) . 12 = q . 4 & (p ^ q) . 13 = q . 5 & (p ^ q) . 14 = q . 6 & (p ^ q) . 15 = q . 7 & (p ^ q) . 16 = q . 8 )
L50:
dom p = {1,2,3,4,5,6,7,8}
by L1, FINSEQ_1:def 3, FINSEQ_3:6;
L51:
dom q = {1,2,3,4,5,6,7,8}
by L1, FINSEQ_1:def 3, FINSEQ_3:6;
( 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 )
by L50, ENUMSET1:def 6;
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 )
by FINSEQ_1:def 7; ( (p ^ q) . 9 = q . 1 & (p ^ q) . 10 = q . 2 & (p ^ q) . 11 = q . 3 & (p ^ q) . 12 = q . 4 & (p ^ q) . 13 = q . 5 & (p ^ q) . 14 = q . 6 & (p ^ q) . 15 = q . 7 & (p ^ q) . 16 = q . 8 )
( 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, ENUMSET1:def 6;
then
( (p ^ q) . (8 + 1) = q . 1 & (p ^ q) . (8 + 2) = q . 2 & (p ^ q) . (8 + 3) = q . 3 & (p ^ q) . (8 + 4) = q . 4 & (p ^ q) . (8 + 5) = q . 5 & (p ^ q) . (8 + 6) = q . 6 & (p ^ q) . (8 + 7) = q . 7 & (p ^ q) . (8 + 8) = q . 8 )
by L1, FINSEQ_1:def 7;
hence
( (p ^ q) . 9 = q . 1 & (p ^ q) . 10 = q . 2 & (p ^ q) . 11 = q . 3 & (p ^ q) . 12 = q . 4 & (p ^ q) . 13 = q . 5 & (p ^ q) . 14 = q . 6 & (p ^ q) . 15 = q . 7 & (p ^ q) . 16 = q . 8 )
; verum