thus ( T is non-absorbing implies for a being adjective of T holds sub (non- a) = sub a ) :: thesis: ( ( for a being adjective of T holds sub (non- a) = sub a ) implies T is non-absorbing )

proof

assume A1: the sub-map of T * the non-op of T = the sub-map of T ; :: according to ABCMIZ_0:def 24 :: thesis: for a being adjective of T holds sub (non- a) = sub a
let a be adjective of T; :: thesis: sub (non- a) = sub a
thus sub (non- a) = sub a by A1, FUNCT_2:15; :: thesis: verum

end;

assume A2: for a being adjective of T holds sub (non- a) = sub a ; :: thesis: T is non-absorbing

now

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 A2
.= 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