let a1, a2, a3, a4, a5, a6, a7, a8, a9, a10 be object ; :: thesis: ( 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 ; :: thesis: ( (<*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 ;
:: thesis: ( (<*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 ;
:: thesis: ( (<*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 ;
:: thesis: ( (<*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 ;
:: thesis: ( (<*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 ;
:: thesis: ( (<*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 ;
:: thesis: ( (<*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 ;
:: thesis: ( (<*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 ;
:: thesis: ( (<*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 ;
:: thesis: (<*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 ;
:: thesis: verum