let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure ; :: thesis: 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; :: thesis: 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, v' be FinSequence of the adjectives of T; :: thesis: ( v is_applicable_to t & rng v' c= rng v implies for s being type of T st s in rng (apply v',t) holds
v ast t <= s )
assume A1:
( v is_applicable_to t & rng v' c= rng v )
; :: thesis: for s being type of T st s in rng (apply v',t) holds
v ast t <= s
let s be type of T; :: thesis: ( s in rng (apply v',t) implies v ast t <= s )
assume
s in rng (apply v',t)
; :: thesis: v ast t <= s
then consider x being set such that
A2:
( x in dom (apply v',t) & s = (apply v',t) . x )
by FUNCT_1:def 5;
A3:
x in Seg (len (apply v',t))
by A2, FINSEQ_1:def 3;
reconsider x = x as Element of NAT by A2;
reconsider x = x as non empty Element of NAT by A3, FINSEQ_1:3;
A4:
x <= len (apply v',t)
by A2, FINSEQ_3:27;
defpred S1[ Nat] means ( $1 <= len (apply v',t) implies for s being type of T st s = (apply v',t) . $1 holds
v ast t <= s );
(apply v',t) . 1 = t
by Def19;
then A5:
S1[1]
by A1, Th44;
A6:
for i being non empty Nat st S1[i] holds
S1[i + 1]
proof
let i be non
empty Nat;
:: thesis: ( S1[i] implies S1[i + 1] )
assume that A7:
S1[
i]
and A8:
i + 1
<= len (apply v',t)
;
:: thesis: for s being type of T st s = (apply v',t) . (i + 1) holds
v ast t <= s
A9:
(
i > 0 &
len (apply v',t) = (len v') + 1 )
by Def19;
then A10:
(
0 + 1
<= i &
i <= len v' )
by A8, NAT_1:13, XREAL_1:8;
then A11:
i in dom v'
by FINSEQ_3:27;
then A12:
(
v' . i in rng v' &
rng v' c= the
adjectives of
T )
by FUNCT_1:12;
then reconsider a =
v' . i as
adjective of
T ;
i < (len v') + 1
by A8, A9, NAT_1:13;
then
i in dom (apply v',t)
by A9, A10, FINSEQ_3:27;
then
(
(apply v',t) . 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) . i as
type of
T ;
A13:
(apply v',t) . (i + 1) = a ast s
by A11, Def19;
(
a in rng v &
rng v c= adjs (v ast t) )
by A1, A12, Th45;
then
(
v ast t <= s &
a in adjs (v ast t) )
by A7, A8, NAT_1:13;
hence
for
s being
type of
T st
s = (apply v',t) . (i + 1) holds
v ast t <= s
by A13, Th24;
:: thesis: verum
end;
for i being non empty Nat holds S1[i]
from NAT_1:sch 10(A5, A6);
hence
v ast t <= s
by A2, A4; :: thesis: verum