thus ( T is non-absorbing implies for a being adjective of T holds sub (non- a) = sub a ) by FUNCT_2:15; :: thesis: ( ( for a being adjective of T holds sub (non- a) = sub a ) implies T is non-absorbing )
assume A1: for a being adjective of T holds sub (non- a) = sub a ; :: thesis: T is non-absorbing

now :: thesis: for x being Element of the adjectives of T holds ( the sub-map of T * the non-op of T) . x = the sub-map of T . x

let x be Element of the adjectives of T; :: thesis: ( the sub-map of T * the non-op of T) . x = the sub-map of T . x
reconsider a = x as adjective of T ;
thus ( the sub-map of T * the non-op of T) . x = sub (non- a) by FUNCT_2:15
.= sub a by A1
.= the sub-map of T . x ; :: thesis: verum

end;

hence the sub-map of T * the non-op of T = the sub-map of T by FUNCT_2:63; :: according to ABCMIZ_0:def 24 :: thesis: verum