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 Function of NAT ,(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 Function of NAT ,(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 l' = l as Element of NAT by ORDINAL1:def 13;
reconsider IT = (fusc . l) /. n as Element of NAT ;
take IT ; :: thesis: ex l being Element of NAT ex fusc being Function of NAT ,(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 l' ; :: thesis: ex fusc being Function of NAT ,(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)))*> ) ) ) )
thus ex fusc being Function of NAT ,(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)))*> ) ) ) ) by A1, Lm3, Lm4; :: thesis: verum