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 i1, i2 being Nat st 1 <= i1 & i1 <= i2 & i2 <= (len v) + 1 holds
for t1, t2 being type of T st t1 = (apply (v,t)) . i1 & t2 = (apply (v,t)) . i2 holds
t2 <= t1
let t be type of T; :: thesis: for v being FinSequence of the adjectives of T st v is_applicable_to t holds
for i1, i2 being Nat st 1 <= i1 & i1 <= i2 & i2 <= (len v) + 1 holds
for t1, t2 being type of T st t1 = (apply (v,t)) . i1 & t2 = (apply (v,t)) . i2 holds
t2 <= t1
let v be FinSequence of the adjectives of T; :: thesis: ( v is_applicable_to t implies for i1, i2 being Nat st 1 <= i1 & i1 <= i2 & i2 <= (len v) + 1 holds
for t1, t2 being type of T st t1 = (apply (v,t)) . i1 & t2 = (apply (v,t)) . i2 holds
t2 <= t1 )
assume A1: for i being Nat
for a being adjective of T
for s being type of T st i in dom v & a = v . i & s = (apply (v,t)) . i holds
a is_applicable_to s ; :: according to ABCMIZ_0:def 21 :: thesis: for i1, i2 being Nat st 1 <= i1 & i1 <= i2 & i2 <= (len v) + 1 holds
for t1, t2 being type of T st t1 = (apply (v,t)) . i1 & t2 = (apply (v,t)) . i2 holds
t2 <= t1
let i1, i2 be Nat; :: thesis: ( 1 <= i1 & i1 <= i2 & i2 <= (len v) + 1 implies for t1, t2 being type of T st t1 = (apply (v,t)) . i1 & t2 = (apply (v,t)) . i2 holds
t2 <= t1 )
assume that
A2: 1 <= i1 and
A3: i1 <= i2 and
A4: i2 <= (len v) + 1 ; :: thesis: for t1, t2 being type of T st t1 = (apply (v,t)) . i1 & t2 = (apply (v,t)) . i2 holds
t2 <= t1
consider j being Nat such that
A5: i2 = i1 + j by A3, NAT_1:10;
let s1, s2 be type of T; :: thesis: ( s1 = (apply (v,t)) . i1 & s2 = (apply (v,t)) . i2 implies s2 <= s1 )
defpred S₁[ Nat] means ( i1 + $1 <= len (apply (v,t)) implies for s being type of T st s = (apply (v,t)) . (i1 + $1) holds
s <= s1 );
A6: len (apply (v,t)) = (len v) + 1 by Def19;
A7: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume that
A8: S₁[i] and
A9: i1 + (i + 1) <= len (apply (v,t)) ; :: thesis: for s being type of T st s = (apply (v,t)) . (i1 + (i + 1)) holds
s <= s1
i1 <= i1 + i by NAT_1:11;
then A10: 1 <= i1 + i by A2, XXREAL_0:2;
A11: i1 + (i + 1) = (i1 + i) + 1 ;
then i1 + i <= len v by A6, A9, XREAL_1:6;
then A12: i1 + i in dom v by A10, FINSEQ_3:25;
then v . (i1 + i) in rng v by FUNCT_1:3;
then reconsider a = v . (i1 + i) as adjective of T ;
i1 + i < (len v) + 1 by A6, A9, A11, NAT_1:13;
then i1 + i in dom (apply (v,t)) by A6, A10, FINSEQ_3:25;
then (apply (v,t)) . (i1 + i) in rng (apply (v,t)) by FUNCT_1:3;
then reconsider s = (apply (v,t)) . (i1 + i) as type of T ;
A13: (apply (v,t)) . ((i1 + i) + 1) = a ast s by A12, Def19;
A14: a ast s <= s by A1, A12, Th20;
s <= s1 by A8, A9, A11, NAT_1:13;
hence for s being type of T st s = (apply (v,t)) . (i1 + (i + 1)) holds
s <= s1 by A13, A14, YELLOW_0:def 2; :: thesis: verum

end;

assume that
A15: s1 = (apply (v,t)) . i1 and
A16: s2 = (apply (v,t)) . i2 ; :: thesis: s2 <= s1
A17: S₁[ 0 ] by A15;
for i being Nat holds S₁[i] from NAT_1:sch 2(A17, A7);
hence s2 <= s1 by A4, A5, A6, A16; :: thesis: verum