let T be non empty reflexive transitive non void TA-structure ; :: thesis: for t being type of T holds <*> the adjectives of T is_applicable_to t
let t be type of T; :: thesis: <*> the adjectives of T is_applicable_to t
let i be natural number ; :: according to ABCMIZ_0:def 21 :: thesis: for a being adjective of T
for s being type of T st i in dom (<*> the adjectives of T) & a = (<*> the adjectives of T) . i & s = (apply (<*> the adjectives of T),t) . i holds
a is_applicable_to s
thus for a being adjective of T
for s being type of T st i in dom (<*> the adjectives of T) & a = (<*> the adjectives of T) . i & s = (apply (<*> the adjectives of T),t) . i holds
a is_applicable_to s ; :: thesis: verum