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 (v1 ^ v2) = (len v1) + (len v2) by FINSEQ_1:22;
A3: rng (v1 ^ v2) = (rng v1) \/ (rng v2) by FINSEQ_1:31;
A4: len (v2 ^ v1) = (len v1) + (len v2) by FINSEQ_1:22;
A5: (len (v1 ^ v2)) + 1 >= 1 by NAT_1:11;
A6: rng (v2 ^ v1) = (rng v1) \/ (rng v2) by FINSEQ_1:31;
len (apply ((v2 ^ v1),t)) = (len (v2 ^ v1)) + 1 by Def19;
then (len (v1 ^ v2)) + 1 in dom (apply ((v2 ^ v1),t)) by A2, A4, A5, FINSEQ_3:25;
then (v2 ^ v1) ast t in rng (apply ((v2 ^ v1),t)) by A2, A4, FUNCT_1:3;
then A7: (v1 ^ v2) ast t <= (v2 ^ v1) ast t by A1, A3, A6, Th46;
len (apply ((v1 ^ v2),t)) = (len (v1 ^ v2)) + 1 by Def19;
then (len (v1 ^ v2)) + 1 in dom (apply ((v1 ^ v2),t)) by A5, FINSEQ_3:25;
then (v1 ^ v2) ast t in rng (apply ((v1 ^ v2),t)) by FUNCT_1:3;
then (v2 ^ v1) ast t <= (v1 ^ v2) ast t by A1, A3, A6, Th46, Th47;
hence (v1 ^ v2) ast t = (v2 ^ v1) ast t by A7, YELLOW_0:def 3; :: thesis: verum