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₁[ Element of 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;
A1: 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 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 & rng {} = {} ) ;
then ( v ast t = t & rng v = {} the adjectives of T ) by Def19, CARD_1:47;
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 Th28; :: thesis: verum

end;

A2: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]

now

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 A4: ( n + 1 = len v & 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 A4, FINSEQ_2:22;
reconsider a = a as adjective of T ;
reconsider B = rng v1 as Subset of the adjectives of T ;
len <*a*> = 1 by FINSEQ_1:57;
then len v = (len v1) + 1 by A5, FINSEQ_1:35;
then ( len v1 = n & v1 is_applicable_to t & <*a*> is_applicable_to v1 ast t ) by A4, A5, Th41;
then A6: ( v1 ast t = B ast t & a is_applicable_to v1 ast t ) by A3, Th40;
let A be Subset of the adjectives of T; :: thesis: ( A = rng v implies v ast t = A ast t )
assume A7: A = rng v ; :: thesis: v ast t = A ast t
then A8: A = B \/ (rng <*a*>) by A5, FINSEQ_1:44
.= B \/ {a} by FINSEQ_1:55 ;
thus v ast t = <*a*> ast (v1 ast t) by A5, Th38
.= a ast (B ast t) by A6, Th32
.= A ast t by A4, A7, A8, Th46, Th56 ; :: thesis: verum

end;

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

end;

A9: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2);
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 )
thus ( 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 ) by A9; :: thesis: verum