let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure ; for t being type of T
for v1, v2 being FinSequence of the adjectives of T st v1 is_applicable_to t & rng v2 c= rng v1 holds
for s being type of T st s in rng (apply (v2,t)) holds
v1 ast t <= s
let t be type of T; for v1, v2 being FinSequence of the adjectives of T st v1 is_applicable_to t & rng v2 c= rng v1 holds
for s being type of T st s in rng (apply (v2,t)) holds
v1 ast t <= s
let v, v9 be FinSequence of the adjectives of T; ( v is_applicable_to t & rng v9 c= rng v implies for s being type of T st s in rng (apply (v9,t)) holds
v ast t <= s )
assume that
A1:
v is_applicable_to t
and
A2:
rng v9 c= rng v
; for s being type of T st s in rng (apply (v9,t)) holds
v ast t <= s
defpred S1[ Nat] means ( $1 <= len (apply (v9,t)) implies for s being type of T st s = (apply (v9,t)) . $1 holds
v ast t <= s );
A3:
for i being non zero Nat st S1[i] holds
S1[i + 1]
proof
A4:
rng v c= adjs (v ast t)
by A1, Th44;
let i be non
zero Nat;
( S1[i] implies S1[i + 1] )
assume that A5:
S1[
i]
and A6:
i + 1
<= len (apply (v9,t))
;
for s being type of T st s = (apply (v9,t)) . (i + 1) holds
v ast t <= s
A7:
0 + 1
<= i
by NAT_1:13;
A8:
len (apply (v9,t)) = (len v9) + 1
by Def19;
then
i < (len v9) + 1
by A6, NAT_1:13;
then
i in dom (apply (v9,t))
by A8, A7, FINSEQ_3:25;
then
(apply (v9,t)) . i in rng (apply (v9,t))
by FUNCT_1:3;
then reconsider s =
(apply (v9,t)) . i as
type of
T ;
A9:
v ast t <= s
by A5, A6, NAT_1:13;
i <= len v9
by A6, A8, XREAL_1:6;
then A10:
i in dom v9
by A7, FINSEQ_3:25;
then A11:
v9 . i in rng v9
by FUNCT_1:3;
then reconsider a =
v9 . i as
adjective of
T ;
A12:
a in rng v
by A2, A11;
(apply (v9,t)) . (i + 1) = a ast s
by A10, Def19;
hence
for
s being
type of
T st
s = (apply (v9,t)) . (i + 1) holds
v ast t <= s
by A12, A4, A9, Th23;
verum
end;
(apply (v9,t)) . 1 = t
by Def19;
then A13:
S1[1]
by A1, Th43;
A14:
for i being non zero Nat holds S1[i]
from NAT_1:sch 10(A13, A3);
let s be type of T; ( s in rng (apply (v9,t)) implies v ast t <= s )
assume
s in rng (apply (v9,t))
; v ast t <= s
then consider x being object such that
A15:
x in dom (apply (v9,t))
and
A16:
s = (apply (v9,t)) . x
by FUNCT_1:def 3;
A17:
x in Seg (len (apply (v9,t)))
by A15, FINSEQ_1:def 3;
reconsider x = x as Element of NAT by A15;
reconsider x = x as non zero Element of NAT by A17, FINSEQ_1:1;
x <= len (apply (v9,t))
by A15, FINSEQ_3:25;
hence
v ast t <= s
by A16, A14; verum