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
rng v c= adjs (v 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
rng v c= adjs (v ast t)
let v be FinSequence of the adjectives of T; :: thesis: ( v is_applicable_to t implies rng v c= adjs (v ast t) )
assume A1: v is_applicable_to t ; :: thesis: rng v c= adjs (v ast t)
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in rng v or a in adjs (v ast t) )
assume A2: a in rng v ; :: thesis: a in adjs (v ast t)
then consider x being set such that
A3: ( x in dom v & a = v . x ) by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A3;
reconsider a = a as adjective of T by A2;
A4: ( x >= 1 & x <= len v ) by A3, FINSEQ_3:27;
len (apply v,t) = (len v) + 1 by Def19;
then ( x < len (apply v,t) & x + 1 <= len (apply v,t) & x + 1 >= 1 ) by A4, NAT_1:13, XREAL_1:8;
then ( x in dom (apply v,t) & x + 1 in dom (apply v,t) ) by A4, FINSEQ_3:27;
then A5: ( (apply v,t) . x in rng (apply v,t) & (apply v,t) . (x + 1) in rng (apply v,t) & rng (apply v,t) c= the carrier of T ) by FUNCT_1:12;
then reconsider s = (apply v,t) . x as type of T ;
a is_applicable_to s by A1, A3, Def21;
then A6: a in adjs (a ast s) by Th22;
a ast s = (apply v,t) . (x + 1) by A3, Def19;
then a ast s >= v ast t by A1, A5, Th43;
then adjs (a ast s) c= adjs (v ast t) by Th10;
hence a in adjs (v ast t) by A6; :: thesis: verum