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