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