let a1, a2, a3, a4, a5, a6, a7, a8, a9, a10 be object ; ( dom (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) = Seg 10 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 1 = a1 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 2 = a2 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 3 = a3 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 4 = a4 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 5 = a5 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 6 = a6 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 7 = a7 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 8 = a8 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 9 = a9 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 10 = a10 )
thus dom (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) =
Seg ((len <*a1,a2,a3,a4,a5,a6,a7,a8*>) + (len <*a9,a10*>))
by FINSEQ_1:def 7
.=
Seg (8 + (len <*a9,a10*>))
by Th19
.=
Seg (8 + 2)
by FINSEQ_1:44
.=
Seg 10
; ( (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 1 = a1 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 2 = a2 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 3 = a3 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 4 = a4 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 5 = a5 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 6 = a6 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 7 = a7 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 8 = a8 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 9 = a9 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 10 = a10 )
A1:
len <*a1,a2,a3,a4,a5,a6,a7,a8*> = 8
by Th19;
then
1 in dom <*a1,a2,a3,a4,a5,a6,a7,a8*>
by FINSEQ_3:25;
hence (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 1 =
<*a1,a2,a3,a4,a5,a6,a7,a8*> . 1
by FINSEQ_1:def 7
.=
a1
by Th19
;
( (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 2 = a2 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 3 = a3 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 4 = a4 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 5 = a5 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 6 = a6 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 7 = a7 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 8 = a8 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 9 = a9 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 10 = a10 )
2 in dom <*a1,a2,a3,a4,a5,a6,a7,a8*>
by A1, FINSEQ_3:25;
hence (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 2 =
<*a1,a2,a3,a4,a5,a6,a7,a8*> . 2
by FINSEQ_1:def 7
.=
a2
by Th19
;
( (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 3 = a3 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 4 = a4 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 5 = a5 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 6 = a6 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 7 = a7 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 8 = a8 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 9 = a9 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 10 = a10 )
3 in dom <*a1,a2,a3,a4,a5,a6,a7,a8*>
by A1, FINSEQ_3:25;
hence (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 3 =
<*a1,a2,a3,a4,a5,a6,a7,a8*> . 3
by FINSEQ_1:def 7
.=
a3
by Th19
;
( (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 4 = a4 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 5 = a5 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 6 = a6 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 7 = a7 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 8 = a8 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 9 = a9 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 10 = a10 )
4 in dom <*a1,a2,a3,a4,a5,a6,a7,a8*>
by A1, FINSEQ_3:25;
hence (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 4 =
<*a1,a2,a3,a4,a5,a6,a7,a8*> . 4
by FINSEQ_1:def 7
.=
a4
by Th19
;
( (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 5 = a5 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 6 = a6 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 7 = a7 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 8 = a8 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 9 = a9 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 10 = a10 )
5 in dom <*a1,a2,a3,a4,a5,a6,a7,a8*>
by A1, FINSEQ_3:25;
hence (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 5 =
<*a1,a2,a3,a4,a5,a6,a7,a8*> . 5
by FINSEQ_1:def 7
.=
a5
by Th19
;
( (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 6 = a6 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 7 = a7 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 8 = a8 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 9 = a9 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 10 = a10 )
6 in dom <*a1,a2,a3,a4,a5,a6,a7,a8*>
by A1, FINSEQ_3:25;
hence (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 6 =
<*a1,a2,a3,a4,a5,a6,a7,a8*> . 6
by FINSEQ_1:def 7
.=
a6
by Th19
;
( (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 7 = a7 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 8 = a8 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 9 = a9 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 10 = a10 )
7 in dom <*a1,a2,a3,a4,a5,a6,a7,a8*>
by A1, FINSEQ_3:25;
hence (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 7 =
<*a1,a2,a3,a4,a5,a6,a7,a8*> . 7
by FINSEQ_1:def 7
.=
a7
by Th19
;
( (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 8 = a8 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 9 = a9 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 10 = a10 )
8 in dom <*a1,a2,a3,a4,a5,a6,a7,a8*>
by A1, FINSEQ_3:25;
hence (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 8 =
<*a1,a2,a3,a4,a5,a6,a7,a8*> . 8
by FINSEQ_1:def 7
.=
a8
by Th19
;
( (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 9 = a9 & (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 10 = a10 )
len <*a9,a10*> = 2
by FINSEQ_1:44;
then
( 1 in dom <*a9,a10*> & 9 = 8 + 1 )
by FINSEQ_3:25;
hence (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 9 =
<*a9,a10*> . 1
by A1, FINSEQ_1:def 7
.=
a9
by FINSEQ_1:44
;
(<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 10 = a10
len <*a9,a10*> = 2
by FINSEQ_1:44;
then
2 in dom <*a9,a10*>
by FINSEQ_3:25;
hence (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9,a10*>) . 10 =
<*a9,a10*> . 2
by A1, FINSEQ_1:def 7
.=
a10
by FINSEQ_1:44
;
verum