set R = Image_hom_Ext_eval (x,F);
( 1. E <> 0. E & 1. (Image_hom_Ext_eval (x,F)) = 1. E & 0. (Image_hom_Ext_eval (x,F)) = 0. E ) by defIm;
hence not Image_hom_Ext_eval (x,F) is degenerated ; :: thesis: verum