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

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

assume A2: a is_properly_applicable_to t ; :: thesis: <*a*> is_properly_applicable_to t
thus <*a*> is_properly_applicable_to t :: thesis: verum

proof

let i be Nat; :: according to ABCMIZ_0:def 28 :: 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_properly_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_properly_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_properly_applicable_to s )
assume i in dom <*a*> ; :: thesis: ( not b = <*a*> . i or not s = (apply (<*a*>,t)) . i or b is_properly_applicable_to s )
then i in Seg 1 by FINSEQ_1:38;
then A3: i = 1 by FINSEQ_1:2, TARSKI:def 1;
thus ( not b = <*a*> . i or not s = (apply (<*a*>,t)) . i or b is_properly_applicable_to s ) by A2, A3, Def19; :: thesis: verum

end;

end;

assume A4: for i being Nat
for a9 being adjective of T
for s being type of T st i in dom <*a*> & a9 = <*a*> . i & s = (apply (<*a*>,t)) . i holds
a9 is_properly_applicable_to s ; :: according to ABCMIZ_0:def 28 :: thesis: a is_properly_applicable_to t
len <*a*> = 1 by FINSEQ_1:40;
then A5: 1 in dom <*a*> by FINSEQ_3:25;
(apply (<*a*>,t)) . 1 = t by Def19;
hence a is_properly_applicable_to t by A4, A5, A1; :: thesis: verum