defpred S₁[ Element of NAT ] means EvenFibs ((2 * $1) + 2) = (EvenFibs (2 * $1)) ^ <*(Fib ((2 * $1) + 2))*>;
let n be Element of NAT ; :: thesis: EvenFibs ((2 * n) + 2) = (EvenFibs (2 * n)) ^ <*(Fib ((2 * n) + 2))*>
A1: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
reconsider ARR = {[1,(FIB . ((2 * k) + 4))]} as FinSubsequence by Th19;
assume S₁[k] ; :: thesis: S₁[k + 1]
set LEFTk = EvenFibs ((2 * (k + 1)) + 2);
set RIGHTk = (EvenFibs (2 * (k + 1))) ^ <*(Fib ((2 * (k + 1)) + 2))*>;
reconsider RS = FIB | (EvenNAT /\ (Seg ((2 * k) + 2))) as FinSubsequence ;
set RR = ((2 * k) + 3) Shift ARR;
A2: (2 * k) + 3 > (2 * k) + 2 by XREAL_1:6;
( dom RS c= EvenNAT /\ (Seg ((2 * k) + 2)) & EvenNAT /\ (Seg ((2 * k) + 2)) c= Seg ((2 * k) + 2) ) by RELAT_1:58, XBOOLE_1:17;
then consider p1 being FinSequence such that
A3: RS c= p1 and
A4: dom p1 = Seg ((2 * k) + 3) by A2, Th21, XBOOLE_1:1;
A5: ex p2 being FinSequence st ARR c= p2 by Th22;
1 + ((2 * k) + 3) = (2 * k) + 4 ;
then A6: ((2 * k) + 3) Shift ARR = {[((2 * k) + 4),(FIB . ((2 * k) + 4))]} by Th20;
len p1 = (2 * k) + 3 by A4, FINSEQ_1:def 3;
then consider RSR being FinSubsequence such that
A7: RSR = RS \/ (((2 * k) + 3) Shift ARR) and
A8: (Seq RS) ^ (Seq ARR) = Seq RSR by A3, A5, PNPROC_1:79;
(EvenFibs (2 * (k + 1))) ^ <*(Fib ((2 * (k + 1)) + 2))*> = (Seq (FIB | (EvenNAT /\ (Seg ((2 * k) + 2))))) ^ <*(FIB . ((2 * k) + 4))*> by Def2
.= Seq RSR by A8, PNPROC_1:3
.= EvenFibs ((2 * (k + 1)) + 2) by A7, A6, Th60 ;
hence S₁[k + 1] ; :: thesis: verum

end;

A9: S₁[ 0 ] by Th23, Th55, Th57, FINSEQ_1:34;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A9, A1);
hence EvenFibs ((2 * n) + 2) = (EvenFibs (2 * n)) ^ <*(Fib ((2 * n) + 2))*> ; :: thesis: verum