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 ^ v2 is_applicable_to t holds
v2 ^ v1 is_applicable_to t
let t be type of T; :: thesis: 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; :: thesis: ( v1 ^ v2 is_applicable_to t implies v2 ^ v1 is_applicable_to t )
assume A1: v1 ^ v2 is_applicable_to t ; :: thesis: v2 ^ v1 is_applicable_to t
let i be natural number ; :: according to ABCMIZ_0:def 21 :: thesis: 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; :: thesis: 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; :: thesis: ( i in dom (v2 ^ v1) & a = (v2 ^ v1) . i & s = (apply (v2 ^ v1),t) . i implies a is_applicable_to s )
assume A2: ( i in dom (v2 ^ v1) & a = (v2 ^ v1) . i & s = (apply (v2 ^ v1),t) . i ) ; :: thesis: a is_applicable_to s
A3: ( i >= 1 & i <= len (v2 ^ v1) & i is Element of NAT ) by A2, FINSEQ_3:27;
A4: ( rng (v1 ^ v2) = (rng v1) \/ (rng v2) & rng (v2 ^ v1) = (rng v1) \/ (rng v2) ) by FINSEQ_1:44;
( i < (len (v2 ^ v1)) + 1 & len (apply (v2 ^ v1),t) = (len (v2 ^ v1)) + 1 ) by A3, Def19, NAT_1:13;
then i in dom (apply (v2 ^ v1),t) by A3, FINSEQ_3:27;
then s in rng (apply (v2 ^ v1),t) by A2, FUNCT_1:12;
then A5: (v1 ^ v2) ast t <= s by A1, A4, Th47;
( a in rng (v2 ^ v1) & rng (v1 ^ v2) c= adjs ((v1 ^ v2) ast t) ) by A1, A2, Th45, FUNCT_1:12;
hence a is_applicable_to s by A4, A5, Th24; :: thesis: verum