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 natural number 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 natural number 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 natural number 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 natural number
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 natural number 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 natural number ; :: 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 A2:
( 1 <= i1 & i1 <= i2 & 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
A3:
i2 = i1 + j
by A2, NAT_1:10;
A4:
j in NAT
by ORDINAL1:def 13;
A5:
len (apply v,t) = (len v) + 1
by Def19;
let s1, s2 be type of T; :: thesis: ( s1 = (apply v,t) . i1 & s2 = (apply v,t) . i2 implies s2 <= s1 )
defpred S1[ Element of 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 );
assume A6:
( s1 = (apply v,t) . i1 & s2 = (apply v,t) . i2 )
; :: thesis: s2 <= s1
then A7:
S1[ 0 ]
;
A8:
for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be
Element of
NAT ;
:: thesis: ( S1[i] implies S1[i + 1] )
assume that A9:
S1[
i]
and A10:
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
A11:
(
i1 <= i1 + i &
i1 + (i + 1) = (i1 + i) + 1 )
by NAT_1:11;
then A12:
( 1
<= i1 + i &
i1 + i <= len v &
i1 + i is
Element of
NAT )
by A2, A5, A10, XREAL_1:8, XXREAL_0:2;
then A13:
i1 + i in dom v
by FINSEQ_3:27;
then
(
v . (i1 + i) in rng v &
rng v c= the
adjectives of
T )
by FUNCT_1:12;
then reconsider a =
v . (i1 + i) as
adjective of
T ;
i1 + i < (len v) + 1
by A5, A10, A11, NAT_1:13;
then
i1 + i in dom (apply v,t)
by A5, A12, FINSEQ_3:27;
then
(
(apply v,t) . (i1 + i) in rng (apply v,t) &
rng (apply v,t) c= the
carrier of
T )
by FUNCT_1:12;
then reconsider s =
(apply v,t) . (i1 + i) as
type of
T ;
A14:
a is_applicable_to s
by A1, A13;
A15:
(apply v,t) . ((i1 + i) + 1) = a ast s
by A13, Def19;
(
s <= s1 &
a ast s <= s )
by A9, A10, A11, A14, Th21, NAT_1:13;
hence
for
s being
type of
T st
s = (apply v,t) . (i1 + (i + 1)) holds
s <= s1
by A15, YELLOW_0:def 2;
:: thesis: verum
end;
for i being Element of NAT holds S1[i]
from NAT_1:sch 1(A7, A8);
hence
s2 <= s1
by A2, A3, A4, A5, A6; :: thesis: verum