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 ^ v2 is_applicable_to t holds
v2 ^ v1 is_applicable_to t
let t be type of T; for v1, v2 being FinSequence of the adjectives of T st v1 ^ v2 is_applicable_to t holds
v2 ^ v1 is_applicable_to t
let v1, v2 be FinSequence of the adjectives of T; ( v1 ^ v2 is_applicable_to t implies v2 ^ v1 is_applicable_to t )
A1:
rng (v1 ^ v2) = (rng v1) \/ (rng v2)
by FINSEQ_1:31;
assume A2:
v1 ^ v2 is_applicable_to t
; v2 ^ v1 is_applicable_to t
then A3:
rng (v1 ^ v2) c= adjs ((v1 ^ v2) ast t)
by Th44;
let i be Nat; ABCMIZ_0:def 21 for a being adjective of T
for s being type of T st i in dom (v2 ^ v1) & a = (v2 ^ v1) . i & s = (apply ((v2 ^ v1),t)) . i holds
a is_applicable_to s
let a be adjective of T; for s being type of T st i in dom (v2 ^ v1) & a = (v2 ^ v1) . i & s = (apply ((v2 ^ v1),t)) . i holds
a is_applicable_to s
let s be type of T; ( i in dom (v2 ^ v1) & a = (v2 ^ v1) . i & s = (apply ((v2 ^ v1),t)) . i implies a is_applicable_to s )
assume that
A4:
i in dom (v2 ^ v1)
and
A5:
a = (v2 ^ v1) . i
and
A6:
s = (apply ((v2 ^ v1),t)) . i
; a is_applicable_to s
A7:
a in rng (v2 ^ v1)
by A4, A5, FUNCT_1:3;
A8:
len (apply ((v2 ^ v1),t)) = (len (v2 ^ v1)) + 1
by Def19;
A9:
rng (v2 ^ v1) = (rng v1) \/ (rng v2)
by FINSEQ_1:31;
i <= len (v2 ^ v1)
by A4, FINSEQ_3:25;
then A10:
i < (len (v2 ^ v1)) + 1
by NAT_1:13;
i >= 1
by A4, FINSEQ_3:25;
then
i in dom (apply ((v2 ^ v1),t))
by A10, A8, FINSEQ_3:25;
then
s in rng (apply ((v2 ^ v1),t))
by A6, FUNCT_1:3;
then
(v1 ^ v2) ast t <= s
by A2, A1, A9, Th46;
hence
a is_applicable_to s
by A1, A9, A7, A3, Th23; verum