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 object ; 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 object such that
A3:
x in dom v
and
A4:
a = v . x
by FUNCT_1:def 3;
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:25;
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:25;
then
x + 1 <= len (apply (v,t))
by A7, XREAL_1:6;
then
x + 1 in dom (apply (v,t))
by A6, FINSEQ_3:25;
then A9:
(apply (v,t)) . (x + 1) in rng (apply (v,t))
by FUNCT_1:3;
x < len (apply (v,t))
by A8, A7, NAT_1:13;
then
x in dom (apply (v,t))
by A5, FINSEQ_3:25;
then
(apply (v,t)) . x in rng (apply (v,t))
by FUNCT_1:3;
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, Th42;
then A10:
adjs (a ast s) c= adjs (v ast t)
by Th10;
a is_applicable_to s
by A1, A3, A4;
then
a in adjs (a ast s)
by Th21;
hence
a in adjs (v ast t)
by A10; verum