let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure ; for t being type of T
for v being FinSequence of the adjectives of T st v is_applicable_to t holds
rng v c= adjs (v ast t)
let t be type of T; for v being FinSequence of the adjectives of T st v is_applicable_to t holds
rng v c= adjs (v ast t)
let v be FinSequence of the adjectives of T; ( v is_applicable_to t implies rng v c= adjs (v ast t) )
assume A1:
v is_applicable_to t
; rng v c= adjs (v ast t)
let a be set ; TARSKI:def 3 ( not a in rng v or a in adjs (v ast t) )
assume A2:
a in rng v
; a in adjs (v ast t)
then consider x being set such that
A3:
x in dom v
and
A4:
a = v . x
by FUNCT_1:def 5;
reconsider a = a as adjective of T by A2;
reconsider x = x as Element of NAT by A3;
A5:
x >= 1
by A3, FINSEQ_3:27;
then A6:
x + 1 >= 1
by NAT_1:13;
A7:
len (apply v,t) = (len v) + 1
by Def19;
A8:
x <= len v
by A3, FINSEQ_3:27;
then
x + 1 <= len (apply v,t)
by A7, XREAL_1:8;
then
x + 1 in dom (apply v,t)
by A6, FINSEQ_3:27;
then A9:
(apply v,t) . (x + 1) in rng (apply v,t)
by FUNCT_1:12;
x < len (apply v,t)
by A8, A7, NAT_1:13;
then
x in dom (apply v,t)
by A5, FINSEQ_3:27;
then
(apply v,t) . x in rng (apply v,t)
by FUNCT_1:12;
then reconsider s = (apply v,t) . x as type of T ;
a ast s = (apply v,t) . (x + 1)
by A3, A4, Def19;
then
a ast s >= v ast t
by A1, A9, Th43;
then A10:
adjs (a ast s) c= adjs (v ast t)
by Th10;
a is_applicable_to s
by A1, A3, A4, Def21;
then
a in adjs (a ast s)
by Th22;
hence
a in adjs (v ast t)
by A10; verum