per cases ( i is Element of NAT or not i is Element of NAT ) ;

suppose i is Element of NAT ; :: thesis: 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 ) )

then reconsider n = i as Element of NAT ;
take Fusc n ; :: thesis: ( ex n being Element of NAT st
( i = n & Fusc n = Fusc n ) or ( i is not Element of NAT & Fusc n = 0 ) )
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: verum

end;

suppose i is not Element of NAT ; :: thesis: 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 ) )

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: verum

end;

end;