reconsider single1 = <*1*> as Element of NAT * by FINSEQ_1:def 11;
consider fusc being sequence of (NAT *) such that
Lm3: fusc . 0 = single1 and
Lm4: for n being Nat holds S₁[n,fusc . n,fusc . (n + 1)] from RECDEF_1:sch 2(Lm1);
thus ( n = 0 implies ex k being Element of NAT st k = 0 ) ; :: thesis: ( not n = 0 implies ex b₁, l being Element of NAT ex fusc being sequence of (NAT *) st
( l + 1 = n & b₁ = (fusc . l) /. n & fusc . 0 = <*1*> & ( for n being Nat holds
( ( for k being Nat st n + 2 = 2 * k holds
fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. k)*> ) & ( for k being Nat st n + 2 = (2 * k) + 1 holds
fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. k) + ((fusc . n) /. (k + 1)))*> ) ) ) ) )
assume n <> 0 ; :: thesis: ex b₁, l being Element of NAT ex fusc being sequence of (NAT *) st
( l + 1 = n & b₁ = (fusc . l) /. n & fusc . 0 = <*1*> & ( for n being Nat holds
( ( for k being Nat st n + 2 = 2 * k holds
fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. k)*> ) & ( for k being Nat st n + 2 = (2 * k) + 1 holds
fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. k) + ((fusc . n) /. (k + 1)))*> ) ) ) )
then consider l being Nat such that
A1: n = l + 1 by NAT_1:6;
reconsider IT = (fusc . l) /. n as Element of NAT ;
reconsider l9 = l as Element of NAT by ORDINAL1:def 12;
take IT ; :: thesis: ex l being Element of NAT ex fusc being sequence of (NAT *) st
( l + 1 = n & IT = (fusc . l) /. n & fusc . 0 = <*1*> & ( for n being Nat holds
( ( for k being Nat st n + 2 = 2 * k holds
fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. k)*> ) & ( for k being Nat st n + 2 = (2 * k) + 1 holds
fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. k) + ((fusc . n) /. (k + 1)))*> ) ) ) )
take l9 ; :: thesis: ex fusc being sequence of (NAT *) st
( l9 + 1 = n & IT = (fusc . l9) /. n & fusc . 0 = <*1*> & ( for n being Nat holds
( ( for k being Nat st n + 2 = 2 * k holds
fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. k)*> ) & ( for k being Nat st n + 2 = (2 * k) + 1 holds
fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. k) + ((fusc . n) /. (k + 1)))*> ) ) ) )
thus ex fusc being sequence of (NAT *) st
( l9 + 1 = n & IT = (fusc . l9) /. n & fusc . 0 = <*1*> & ( for n being Nat holds
( ( for k being Nat st n + 2 = 2 * k holds
fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. k)*> ) & ( for k being Nat st n + 2 = (2 * k) + 1 holds
fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. k) + ((fusc . n) /. (k + 1)))*> ) ) ) ) by A1, Lm3, Lm4; :: thesis: verum