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

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

then A2: dom the non-op of A = the adjectives of A ;
a = {} by A1, SUBSET_1:def 1;
hence the non-op of A . a is adjective of A by A1, A2, FUNCT_1:def 2; :: 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:5; :: thesis: verum

end;

end;