A1: len (even-seq 1) = 1 by Def1;
dom (even-seq 1) = Seg (len (even-seq 1)) by FINSEQ_1:def 3
.= Seg 1 by Def1 ;
then 1 in dom (even-seq 1) ;
then A2: (even-seq 1) . 1 = 2 * 1 by Def1;
A3: even-seq (1 + 1) = (even-seq 1) ^ <*(2 * (1 + 1))*> by Th3;
even-seq (2 + 1) = (even-seq 2) ^ <*(2 * (2 + 1))*> by Th3;
hence ( even-seq 1 = <*2*> & even-seq 2 = <*2,4*> & even-seq 3 = <*2,4,6*> ) by FINSEQ_1:40, A1, A2, A3; :: thesis: verum