let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure ; :: thesis: for t being type of T
for v being FinSequence of the adjectives of T st v is_applicable_to t holds
for A being Subset of the adjectives of T st A = rng v holds
v ast t = A ast t
defpred S₁[ Nat] means for t being type of T
for v being FinSequence of the adjectives of T st $1 = len v & v is_applicable_to t holds
for A being Subset of the adjectives of T st A = rng v holds
v ast t = A ast t;
let t be type of T; :: thesis: for v being FinSequence of the adjectives of T st v is_applicable_to t holds
for A being Subset of the adjectives of T st A = rng v holds
v ast t = A ast t
let v be FinSequence of the adjectives of T; :: thesis: ( v is_applicable_to t implies for A being Subset of the adjectives of T st A = rng v holds
v ast t = A ast t )

A1: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]

now :: thesis: for t being type of T
for v being FinSequence of the adjectives of T st n + 1 = len v & v is_applicable_to t holds
for A being Subset of the adjectives of T st A = rng v holds
v ast t = A ast t

let t be type of T; :: thesis: for v being FinSequence of the adjectives of T st n + 1 = len v & v is_applicable_to t holds
for A being Subset of the adjectives of T st A = rng v holds
v ast t = A ast t
let v be FinSequence of the adjectives of T; :: thesis: ( n + 1 = len v & v is_applicable_to t implies for A being Subset of the adjectives of T st A = rng v holds
v ast t = A ast t )
assume that
A3: n + 1 = len v and
A4: v is_applicable_to t ; :: thesis: for A being Subset of the adjectives of T st A = rng v holds
v ast t = A ast t
consider v1 being FinSequence of the adjectives of T, a being Element of the adjectives of T such that
A5: v = v1 ^ <*a*> by A3, FINSEQ_2:19;
reconsider B = rng v1 as Subset of the adjectives of T ;
reconsider a = a as adjective of T ;
len <*a*> = 1 by FINSEQ_1:40;
then A6: len v = (len v1) + 1 by A5, FINSEQ_1:22;
v1 is_applicable_to t by A4, A5, Th40;
then A7: v1 ast t = B ast t by A2, A3, A6;
let A be Subset of the adjectives of T; :: thesis: ( A = rng v implies v ast t = A ast t )
assume A8: A = rng v ; :: thesis: v ast t = A ast t
then A9: A = B \/ (rng <*a*>) by A5, FINSEQ_1:31
.= B \/ {a} by FINSEQ_1:38 ;
thus v ast t = <*a*> ast (v1 ast t) by A5, Th37
.= a ast (B ast t) by A7, Th31
.= A ast t by A4, A8, A9, Th45, Th55 ; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

A10: S₁[ 0 ]

proof

let t be type of T; :: thesis: for v being FinSequence of the adjectives of T st 0 = len v & v is_applicable_to t holds
for A being Subset of the adjectives of T st A = rng v holds
v ast t = A ast t
let v be FinSequence of the adjectives of T; :: thesis: ( 0 = len v & v is_applicable_to t implies for A being Subset of the adjectives of T st A = rng v holds
v ast t = A ast t )
assume A11: 0 = len v ; :: thesis: ( not v is_applicable_to t or for A being Subset of the adjectives of T st A = rng v holds
v ast t = A ast t )
then v = <*> the adjectives of T ;
then A12: rng v = {} the adjectives of T ;
v ast t = t by A11, Def19;
hence ( not v is_applicable_to t or for A being Subset of the adjectives of T st A = rng v holds
v ast t = A ast t ) by A12, Th27; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A10, A1);
hence ( v is_applicable_to t implies for A being Subset of the adjectives of T st A = rng v holds
v ast t = A ast t ) ; :: thesis: verum