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
(v1 ^ v2) ast t = (v2 ^ v1) ast 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
(v1 ^ v2) ast t = (v2 ^ v1) ast t
let v1, v2 be FinSequence of the adjectives of T; :: thesis: ( v1 ^ v2 is_applicable_to t implies (v1 ^ v2) ast t = (v2 ^ v1) ast t )
assume A1: v1 ^ v2 is_applicable_to t ; :: thesis: (v1 ^ v2) ast t = (v2 ^ v1) ast t
A2: ( len (apply (v1 ^ v2),t) = (len (v1 ^ v2)) + 1 & len (apply (v2 ^ v1),t) = (len (v2 ^ v1)) + 1 ) by Def19;
A3: ( len (v1 ^ v2) = (len v1) + (len v2) & len (v2 ^ v1) = (len v1) + (len v2) ) by FINSEQ_1:35;
A4: ( rng (v1 ^ v2) = (rng v1) \/ (rng v2) & rng (v2 ^ v1) = (rng v1) \/ (rng v2) ) by FINSEQ_1:44;
(len (v1 ^ v2)) + 1 >= 1 by NAT_1:11;
then ( (len (v1 ^ v2)) + 1 in dom (apply (v1 ^ v2),t) & (len (v1 ^ v2)) + 1 in dom (apply (v2 ^ v1),t) ) by A2, A3, FINSEQ_3:27;
then ( (v1 ^ v2) ast t in rng (apply (v1 ^ v2),t) & (v2 ^ v1) ast t in rng (apply (v2 ^ v1),t) ) by A3, FUNCT_1:12;
then ( (v1 ^ v2) ast t <= (v2 ^ v1) ast t & (v2 ^ v1) ast t <= (v1 ^ v2) ast t ) by A1, A4, Th47, Th48;
hence (v1 ^ v2) ast t = (v2 ^ v1) ast t by YELLOW_0:def 3; :: thesis: verum