per cases ;

suppose i is Element of NAT ; :: thesis:

then reconsider n = i as Element of NAT ;
take Fusc n ; :: thesis:
thus ( ex n being Element of NAT st
( i = n & Fusc n = Fusc n ) or ( i is not Element of NAT & Fusc n = 0 ) ) ; :: thesis:

end;

suppose i is not Element of NAT ; :: thesis:

hence ex b₁ being Element of NAT st
( ex n being Element of NAT st
( i = n & b₁ = Fusc n ) or ( i is not Element of NAT & b₁ = 0 ) ) ; :: thesis:

end;

end;