let T be non empty reflexive transitive non void TA-structure ; :: thesis: for t being type of T
for a being adjective of T holds
( a is_applicable_to t iff <*a*> is_applicable_to t )
let t be type of T; :: thesis: for a being adjective of T holds
( a is_applicable_to t iff <*a*> is_applicable_to t )
let a be adjective of T; :: thesis: ( a is_applicable_to t iff <*a*> is_applicable_to t )
set v = <*a*>;

hereby :: thesis: ( <*a*> is_applicable_to t implies a is_applicable_to t )

assume A1: a is_applicable_to t ; :: thesis: <*a*> is_applicable_to t
thus <*a*> is_applicable_to t :: thesis: verum

proof

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 <*a*> & a = <*a*> . i & s = (apply <*a*>,t) . i holds
a is_applicable_to s
let b be adjective of T; :: thesis: for s being type of T st i in dom <*a*> & b = <*a*> . i & s = (apply <*a*>,t) . i holds
b is_applicable_to s
let s be type of T; :: thesis: ( i in dom <*a*> & b = <*a*> . i & s = (apply <*a*>,t) . i implies b is_applicable_to s )
assume i in dom <*a*> ; :: thesis: ( not b = <*a*> . i or not s = (apply <*a*>,t) . i or b is_applicable_to s )
then i in Seg 1 by FINSEQ_1:55;
then i = 1 by FINSEQ_1:4, TARSKI:def 1;
then ( <*a*> . i = a & (apply <*a*>,t) . i = t ) by Def19, FINSEQ_1:57;
hence ( not b = <*a*> . i or not s = (apply <*a*>,t) . i or b is_applicable_to s ) by A1; :: thesis: verum

end;

end;

assume A2: for i being natural number
for a' being adjective of T
for s being type of T st i in dom <*a*> & a' = <*a*> . i & s = (apply <*a*>,t) . i holds
a' is_applicable_to s ; :: according to ABCMIZ_0:def 21 :: thesis: a is_applicable_to t
len <*a*> = 1 by FINSEQ_1:57;
then ( 1 in dom <*a*> & <*a*> . 1 = a & (apply <*a*>,t) . 1 = t ) by Def19, FINSEQ_1:57, FINSEQ_3:27;
hence a is_applicable_to t by A2; :: thesis: verum