let n be non zero Nat; :: thesis: even-seq (n + 1) = (even-seq n) ^ <*(2 * (n + 1))*>
set p = even-seq (n + 1);
set q = even-seq n;
set x = <*(2 * (n + 1))*>;
A1: len (even-seq (n + 1)) = n + 1 by Def1;
A2: len (even-seq n) = n by Def1;
then A3: len (even-seq (n + 1)) = len ((even-seq n) ^ <*(2 * (n + 1))*>) by A1, FINSEQ_2:16;
A4: dom (even-seq n) = Seg n by Th1;
A5: dom (even-seq (n + 1)) = Seg (n + 1) by A1, FINSEQ_1:def 3;
for k being Nat st 1 <= k & k <= len (even-seq (n + 1)) holds
(even-seq (n + 1)) . k = ((even-seq n) ^ <*(2 * (n + 1))*>) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len (even-seq (n + 1)) implies (even-seq (n + 1)) . k = ((even-seq n) ^ <*(2 * (n + 1))*>) . k )
assume ( 1 <= k & k <= len (even-seq (n + 1)) ) ; :: thesis: (even-seq (n + 1)) . k = ((even-seq n) ^ <*(2 * (n + 1))*>) . k

per cases then ( ( 1 <= k & k < n + 1 ) or k = n + 1 ) by A1, XXREAL_0:1;

suppose A7: ( 1 <= k & k < n + 1 ) ; :: thesis: (even-seq (n + 1)) . k = ((even-seq n) ^ <*(2 * (n + 1))*>) . k

then k <= n by NAT_1:13;
then A9: k in dom (even-seq n) by A4, A7;
A10: k in dom (even-seq (n + 1)) by A5, A7;
((even-seq n) ^ <*(2 * (n + 1))*>) . k = (even-seq n) . k by A9, FINSEQ_1:def 7
.= 2 * k by A9, Def1 ;
hence (even-seq (n + 1)) . k = ((even-seq n) ^ <*(2 * (n + 1))*>) . k by A10, Def1; :: thesis: verum

end;

suppose k = n + 1 ; :: thesis: (even-seq (n + 1)) . k = ((even-seq n) ^ <*(2 * (n + 1))*>) . k

hence (even-seq (n + 1)) . k = ((even-seq n) ^ <*(2 * (n + 1))*>) . k by A2, Def1, A5, FINSEQ_1:4; :: thesis: verum

end;

end;

end;

hence even-seq (n + 1) = (even-seq n) ^ <*(2 * (n + 1))*> by A3, FINSEQ_1:14; :: thesis: verum