reconsider single1 = <*1*> as Element of NAT * by FINSEQ_1:def 11;
consider fusc being sequence of (NAT *) such that
fusc . 0 = single1 and
for n being Nat holds S₁[n,fusc . n,fusc . (n + 1)] from RECDEF_1:sch 2(Lm1);
let n1, n2 be Element of NAT ; :: thesis: ( ( n = 0 & n1 = 0 & n2 = 0 implies n1 = n2 ) & ( not n = 0 & ex l being Element of NAT ex fusc being sequence of (NAT *) st
( l + 1 = n & n1 = (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)))*> ) ) ) ) & ex l being Element of NAT ex fusc being sequence of (NAT *) st
( l + 1 = n & n2 = (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)))*> ) ) ) ) implies n1 = n2 ) )
thus ( n = 0 & n1 = 0 & n2 = 0 implies n1 = n2 ) ; :: thesis: ( not n = 0 & ex l being Element of NAT ex fusc being sequence of (NAT *) st
( l + 1 = n & n1 = (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)))*> ) ) ) ) & ex l being Element of NAT ex fusc being sequence of (NAT *) st
( l + 1 = n & n2 = (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)))*> ) ) ) ) implies n1 = n2 )
assume n <> 0 ; :: thesis: ( for l being Element of NAT
for fusc being sequence of (NAT *) holds
( not l + 1 = n or not n1 = (fusc . l) /. n or not fusc . 0 = <*1*> or ex n being Nat st
( ( for k being Nat st n + 2 = 2 * k holds
fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. k)*> ) implies ex k being Nat st
( n + 2 = (2 * k) + 1 & not fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. k) + ((fusc . n) /. (k + 1)))*> ) ) ) or for l being Element of NAT
for fusc being sequence of (NAT *) holds
( not l + 1 = n or not n2 = (fusc . l) /. n or not fusc . 0 = <*1*> or ex n being Nat st
( ( for k being Nat st n + 2 = 2 * k holds
fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. k)*> ) implies ex k being Nat st
( n + 2 = (2 * k) + 1 & not fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. k) + ((fusc . n) /. (k + 1)))*> ) ) ) or n1 = n2 )
given l1 being Element of NAT , fusc1 being sequence of (NAT *) such that A2: ( l1 + 1 = n & n1 = (fusc1 . l1) /. n ) and
A3: fusc1 . 0 = <*1*> and
A4: for n being Nat holds
( ( for k being Nat st n + 2 = 2 * k holds
fusc1 . (n + 1) = (fusc1 . n) ^ <*((fusc1 . n) /. k)*> ) & ( for k being Nat st n + 2 = (2 * k) + 1 holds
fusc1 . (n + 1) = (fusc1 . n) ^ <*(((fusc1 . n) /. k) + ((fusc1 . n) /. (k + 1)))*> ) ) ; :: thesis: ( for l being Element of NAT
for fusc being sequence of (NAT *) holds
( not l + 1 = n or not n2 = (fusc . l) /. n or not fusc . 0 = <*1*> or ex n being Nat st
( ( for k being Nat st n + 2 = 2 * k holds
fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. k)*> ) implies ex k being Nat st
( n + 2 = (2 * k) + 1 & not fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. k) + ((fusc . n) /. (k + 1)))*> ) ) ) or n1 = n2 )
A5: fusc1 . 0 = single1 by A3;
A6: for n being Nat holds S₂[n,fusc1 . n,fusc1 . (n + 1)] by A4;
given l2 being Element of NAT , fusc2 being sequence of (NAT *) such that A7: ( l2 + 1 = n & n2 = (fusc2 . l2) /. n ) and
A8: fusc2 . 0 = <*1*> and
A9: for n being Nat holds
( ( for k being Nat st n + 2 = 2 * k holds
fusc2 . (n + 1) = (fusc2 . n) ^ <*((fusc2 . n) /. k)*> ) & ( for k being Nat st n + 2 = (2 * k) + 1 holds
fusc2 . (n + 1) = (fusc2 . n) ^ <*(((fusc2 . n) /. k) + ((fusc2 . n) /. (k + 1)))*> ) ) ; :: thesis: n1 = n2
A10: for n being Nat holds S₂[n,fusc2 . n,fusc2 . (n + 1)] by A9;
A11: fusc2 . 0 = single1 by A8;
fusc1 = fusc2 from NAT_1:sch 14(A5, A6, A11, A10, Lm2);
hence n1 = n2 by A2, A7; :: thesis: verum