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
(v1 ^ v2) ast t = (v2 ^ v1) ast 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
(v1 ^ v2) ast t = (v2 ^ v1) ast t
let v1, v2 be FinSequence of the adjectives of T; ( v1 ^ v2 is_applicable_to t implies (v1 ^ v2) ast t = (v2 ^ v1) ast t )
assume A1:
v1 ^ v2 is_applicable_to t
; (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; verum