( 0. (Image f) = 0. E & 1. (Image f) = 1. E ) by RING_2:def 6;
hence 0. (Image f) <> 1. (Image f) ; :: according to STRUCT_0:def 8 :: thesis: verum