per cases ( the adjectives of A is empty or not the adjectives of A is empty ) ;

suppose the adjectives of A is empty ; :: thesis: the non-op of A . a is adjective of A

then ( a = {} & not a in the adjectives of A & dom the non-op of A = the adjectives of A ) by SUBSET_1:def 2;
hence the non-op of A . a is adjective of A by FUNCT_1:def 4; :: thesis: verum

end;

suppose not the adjectives of A is empty ; :: thesis: the non-op of A . a is adjective of A

hence the non-op of A . a is adjective of A by FUNCT_2:7; :: thesis: verum

end;

end;