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

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
reconsider ARR = {[1,(FIB . ((2 * k) + 5))]} as FinSubsequence by Th17;
assume S₁[k] ; :: thesis: S₁[k + 1]
set LEFTk = OddFibs ((2 * (k + 1)) + 3);
set RIGHTk = (OddFibs ((2 * (k + 1)) + 1)) ^ <*(Fib ((2 * (k + 1)) + 3))*>;
reconsider RS = FIB | (OddNAT /\ (Seg ((2 * k) + 3))) as FinSubsequence ;
set RR = Shift (ARR,((2 * k) + 4));
A2: (2 * k) + 4 > (2 * k) + 3 by XREAL_1:6;
( dom RS c= OddNAT /\ (Seg ((2 * k) + 3)) & OddNAT /\ (Seg ((2 * k) + 3)) c= Seg ((2 * k) + 3) ) 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) + 4) by A2, Th19, XBOOLE_1:1;
A5: ex p2 being FinSequence st ARR c= p2 by Th20;
1 + ((2 * k) + 4) = (2 * k) + 5 ;
then A6: Shift (ARR,((2 * k) + 4)) = {[((2 * k) + 5),(FIB . ((2 * k) + 5))]} by Th18;
len p1 = (2 * k) + 4 by A4, FINSEQ_1:def 3;
then consider RSR being FinSubsequence such that
A7: RSR = RS \/ (Shift (ARR,((2 * k) + 4))) and
A8: (Seq RS) ^ (Seq ARR) = Seq RSR by A3, A5, VALUED_1:64;
(OddFibs ((2 * (k + 1)) + 1)) ^ <*(Fib ((2 * (k + 1)) + 3))*> = (Seq (FIB | (OddNAT /\ (Seg ((2 * k) + 3))))) ^ <*(FIB . ((2 * k) + 5))*> by Def2
.= Seq RSR by A8, FINSEQ_3:157
.= OddFibs ((2 * (k + 1)) + 3) by A7, A6, Th63 ;
hence S₁[k + 1] ; :: thesis: verum

end;

A9: S₁[ 0 ] by Th22, Th60, Th61;
for k being Nat holds S₁[k] from NAT_1:sch 2(A9, A1);
hence OddFibs ((2 * n) + 3) = (OddFibs ((2 * n) + 1)) ^ <*(Fib ((2 * n) + 3))*> ; :: thesis: verum