A1: 0c = 0 ;
thus ( ( m <= k implies 1 is Element of COMPLEX ) & ( not m <= k implies 0 is Element of COMPLEX ) & ( for b₁ being Element of COMPLEX holds verum ) ) by A1, COMPLEX1:def 7; :: thesis: verum