now :: thesis: ( b is Integer implies ex c being set ex k being Integer st
( k = b & c = a #Z k ) )

assume b is Integer ; :: thesis: ex c being set ex k being Integer st
( k = b & c = a #Z k )
then reconsider k = b as Integer ;
take c = a #Z k; :: thesis: ex k being Integer st
( k = b & c = a #Z k )
thus ex k being Integer st
( k = b & c = a #Z k ) ; :: thesis: verum

end;

hence ( ( a > 0 implies ex b₁ being Real st b₁ = a #R b ) & ( a = 0 & b > 0 implies ex b₁ being Real st b₁ = 0 ) & ( b is Integer implies ex b₁ being Real ex k being Integer st
( k = b & b₁ = a #Z k ) ) ) ; :: thesis: verum