let T be non empty reflexive transitive non void TAS-structure ; :: thesis: for t being type of T
for v being FinSequence of the adjectives of T st v is_properly_applicable_to t holds
v is_applicable_to t
let t be type of T; :: thesis: for v being FinSequence of the adjectives of T st v is_properly_applicable_to t holds
v is_applicable_to t
let v be FinSequence of the adjectives of T; :: thesis: ( v is_properly_applicable_to t implies v is_applicable_to t )
assume A1: for i being Nat
for a being adjective of T
for s being type of T st i in dom v & a = v . i & s = (apply (v,t)) . i holds
a is_properly_applicable_to s ; :: according to ABCMIZ_0:def 28 :: thesis: v is_applicable_to t
let i be Nat; :: according to ABCMIZ_0:def 21 :: thesis: for a being adjective of T
for s being type of T st i in dom v & a = v . i & s = (apply (v,t)) . i holds
a is_applicable_to s
let a be adjective of T; :: thesis: for s being type of T st i in dom v & a = v . i & s = (apply (v,t)) . i holds
a is_applicable_to s
let s be type of T; :: thesis: ( i in dom v & a = v . i & s = (apply (v,t)) . i implies a is_applicable_to s )
assume that
A2: i in dom v and
A3: a = v . i and
A4: s = (apply (v,t)) . i ; :: thesis: a is_applicable_to s
a is_properly_applicable_to s by A1, A2, A3, A4;
hence a is_applicable_to s ; :: thesis: verum