thus A1: Fusc 0 = 0 by Def2; :: thesis: ( Fusc 1 = 1 & ( for n being Nat holds
( Fusc (2 * n) = Fusc n & Fusc ((2 * n) + 1) = (Fusc n) + (Fusc (n + 1)) ) ) )
( 0 + 1 = 1 & 1 = <*1*> /. 1 ) by FINSEQ_4:25;
hence Fusc 1 = 1 by Def2, Lm3, Lm4; :: thesis: for n being Nat holds
( Fusc (2 * n) = Fusc n & Fusc ((2 * n) + 1) = (Fusc n) + (Fusc (n + 1)) )
let n be Nat; :: thesis: ( Fusc (2 * n) = Fusc n & Fusc ((2 * n) + 1) = (Fusc n) + (Fusc (n + 1)) )

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: ( Fusc (2 * n) = Fusc n & Fusc ((2 * n) + 1) = (Fusc n) + (Fusc (n + 1)) )

hence ( Fusc (2 * n) = Fusc n & Fusc ((2 * n) + 1) = (Fusc n) + (Fusc (n + 1)) ) by A1; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: ( Fusc (2 * n) = Fusc n & Fusc ((2 * n) + 1) = (Fusc n) + (Fusc (n + 1)) )

then consider l being Nat such that
A2: n = l + 1 by NAT_1:6;
reconsider l = l, n1 = n as Element of NAT by ORDINAL1:def 13;
defpred S₃[ Element of NAT ] means ( len (fusc . $1) = $1 + 1 & ( for k being Element of NAT st k <= $1 holds
(fusc . $1) /. (k + 1) = Fusc (k + 1) ) );
A3: S₃[ 0 ]

proof

thus len (fusc . 0 ) = 0 + 1 by Lm3, FINSEQ_1:57; :: thesis: for k being Element of NAT st k <= 0 holds
(fusc . 0 ) /. (k + 1) = Fusc (k + 1)
let k be Element of NAT ; :: thesis: ( k <= 0 implies (fusc . 0 ) /. (k + 1) = Fusc (k + 1) )
assume k <= 0 ; :: thesis: (fusc . 0 ) /. (k + 1) = Fusc (k + 1)
then k = 0 ;
hence (fusc . 0 ) /. (k + 1) = Fusc (k + 1) by Def2, Lm3, Lm4; :: thesis: verum

end;

A4: for n being Element of NAT st S₃[n] holds
S₃[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₃[n] implies S₃[n + 1] )
assume A5: ( len (fusc . n) = n + 1 & ( for k being Element of NAT st k <= n holds
(fusc . n) /. (k + 1) = Fusc (k + 1) ) ) ; :: thesis: S₃[n + 1]
n + 2 = (2 * ((n + 2) div 2)) + ((n + 2) mod 2) by NAT_D:2;
then A6: ( n + 2 = (2 * ((n + 2) div 2)) + 0 or n + 2 = (2 * ((n + 2) div 2)) + 1 ) by NAT_D:12;
A7: ( len <*(((fusc . n) /. ((n + 2) div 2)) + ((fusc . n) /. (((n + 2) div 2) + 1)))*> = 1 & len <*((fusc . n) /. ((n + 2) div 2))*> = 1 ) by FINSEQ_1:57;

per cases ( n + 2 = 2 * ((n + 2) div 2) or n + 2 = (2 * ((n + 2) div 2)) + 1 ) by A6;

suppose n + 2 = 2 * ((n + 2) div 2) ; :: thesis: S₃[n + 1]

then A8: fusc . (n + 1) = (fusc . n) ^ <*((fusc . n) /. ((n + 2) div 2))*> by Lm4;
hence len (fusc . (n + 1)) = (n + 1) + 1 by A5, A7, FINSEQ_1:35; :: thesis: for k being Element of NAT st k <= n + 1 holds
(fusc . (n + 1)) /. (k + 1) = Fusc (k + 1)
let k be Element of NAT ; :: thesis: ( k <= n + 1 implies (fusc . (n + 1)) /. (k + 1) = Fusc (k + 1) )
assume k <= n + 1 ; :: thesis: (fusc . (n + 1)) /. (k + 1) = Fusc (k + 1)
then A9: ( k = n + 1 or k <= n ) by NAT_1:8;

now

assume A10: k <= n ; :: thesis: (fusc . (n + 1)) /. (k + 1) = Fusc (k + 1)
then ( 0 + 1 <= k + 1 & k + 1 <= n + 1 ) by XREAL_1:9;
then k + 1 in dom (fusc . n) by A5, FINSEQ_3:27;
hence (fusc . (n + 1)) /. (k + 1) = (fusc . n) /. (k + 1) by A8, FINSEQ_4:83
.= Fusc (k + 1) by A5, A10 ;
:: thesis: verum

end;

hence (fusc . (n + 1)) /. (k + 1) = Fusc (k + 1) by A9, Def2, Lm3, Lm4; :: thesis: verum

end;

suppose n + 2 = (2 * ((n + 2) div 2)) + 1 ; :: thesis: S₃[n + 1]

then A11: fusc . (n + 1) = (fusc . n) ^ <*(((fusc . n) /. ((n + 2) div 2)) + ((fusc . n) /. (((n + 2) div 2) + 1)))*> by Lm4;
hence len (fusc . (n + 1)) = (n + 1) + 1 by A5, A7, FINSEQ_1:35; :: thesis: for k being Element of NAT st k <= n + 1 holds
(fusc . (n + 1)) /. (k + 1) = Fusc (k + 1)
let k be Element of NAT ; :: thesis: ( k <= n + 1 implies (fusc . (n + 1)) /. (k + 1) = Fusc (k + 1) )
assume k <= n + 1 ; :: thesis: (fusc . (n + 1)) /. (k + 1) = Fusc (k + 1)
then A12: ( k = n + 1 or k <= n ) by NAT_1:8;

now

assume A13: k <= n ; :: thesis: (fusc . (n + 1)) /. (k + 1) = Fusc (k + 1)
then ( 0 + 1 <= k + 1 & k + 1 <= n + 1 ) by XREAL_1:9;
then k + 1 in dom (fusc . n) by A5, FINSEQ_3:27;
hence (fusc . (n + 1)) /. (k + 1) = (fusc . n) /. (k + 1) by A11, FINSEQ_4:83
.= Fusc (k + 1) by A5, A13 ;
:: thesis: verum

end;

hence (fusc . (n + 1)) /. (k + 1) = Fusc (k + 1) by A12, Def2, Lm3, Lm4; :: thesis: verum

end;

end;

end;

A14: for n being Element of NAT holds S₃[n] from NAT_1:sch 1(A3, A4);
l + l = (1 + 1) * l ;
then A15: l <= 2 * l by NAT_1:11;
A16: ( len (fusc . (2 * l)) = (2 * l) + 1 & len (fusc . ((2 * l) + 1)) = ((2 * l) + 1) + 1 ) by A14;
A17: ( 2 * n = (2 * l) + (2 * 1) & (2 * l) + (1 + 1) = ((2 * l) + 1) + 1 & ((2 * l) + 1) + 1 <> 0 & ((2 * l) + 1) + (1 + 1) = (((2 * l) + 1) + 1) + 1 ) by A2;
then fusc . ((2 * l) + 1) = (fusc . (2 * l)) ^ <*((fusc . (2 * l)) /. n1)*> by Lm4;
hence Fusc (2 * n) = ((fusc . (2 * l)) ^ <*((fusc . (2 * l)) /. n)*>) /. (((2 * l) + 1) + 1) by A2, Def2, Lm3, Lm4
.= (fusc . (2 * l)) /. n by A16, FINSEQ_4:82
.= Fusc n by A2, A14, A15 ;
:: thesis: Fusc ((2 * n) + 1) = (Fusc n) + (Fusc (n + 1))
A18: fusc . (2 * n1) = (fusc . ((2 * l) + 1)) ^ <*(((fusc . ((2 * l) + 1)) /. n1) + ((fusc . ((2 * l) + 1)) /. (n1 + 1)))*> by A17, Lm4;
2 * l <= (2 * l) + 1 by NAT_1:11;
then ( l <= (2 * l) + 1 & l + 1 <= (2 * l) + 1 ) by A15, XREAL_1:9, XXREAL_0:2;
then A19: ( Fusc n = (fusc . ((2 * l) + 1)) /. n & Fusc (n + 1) = (fusc . ((2 * l) + 1)) /. (n + 1) ) by A2, A14;
thus Fusc ((2 * n) + 1) = (fusc . (2 * n)) /. ((2 * n) + 1) by Def2, Lm3, Lm4
.= (Fusc n) + (Fusc (n + 1)) by A2, A16, A18, A19, FINSEQ_4:82 ; :: thesis: verum

end;

end;