let T be non empty reflexive transitive non void 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 is_applicable_to t & v2 is_applicable_to 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 is_applicable_to t & v2 is_applicable_to v1 ast t )
let v1, v2 be FinSequence of the adjectives of T; :: thesis: ( v1 ^ v2 is_applicable_to t implies ( v1 is_applicable_to t & v2 is_applicable_to v1 ast t ) )
set v = v1 ^ v2;
assume A1: for i being natural number
for a being adjective of T
for s being type of T st i in dom (v1 ^ v2) & a = (v1 ^ v2) . i & s = (apply (v1 ^ v2),t) . i holds
a is_applicable_to s ; :: according to ABCMIZ_0:def 21 :: thesis: ( v1 is_applicable_to t & v2 is_applicable_to v1 ast t )

hereby :: according to ABCMIZ_0:def 21 :: thesis: v2 is_applicable_to v1 ast t

let i be natural number ; :: thesis: for a being adjective of T
for s being type of T st i in dom v1 & a = v1 . i & s = (apply 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 v1 & a = v1 . i & s = (apply v1,t) . i holds
a is_applicable_to s
let s be type of T; :: thesis: ( i in dom v1 & a = v1 . i & s = (apply v1,t) . i implies a is_applicable_to s )
assume A2: ( i in dom v1 & a = v1 . i & s = (apply v1,t) . i ) ; :: thesis: a is_applicable_to s
dom v1 c= dom (v1 ^ v2) by FINSEQ_1:39;
then ( i in dom (v1 ^ v2) & a = (v1 ^ v2) . i & s = (apply (v1 ^ v2),t) . i ) by A2, Th36, FINSEQ_1:def 7;
hence a is_applicable_to s by A1; :: thesis: verum

end;

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 & a = v2 . i & s = (apply v2,(v1 ast 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 & a = v2 . i & s = (apply v2,(v1 ast t)) . i holds
a is_applicable_to s
let s be type of T; :: thesis: ( i in dom v2 & a = v2 . i & s = (apply v2,(v1 ast t)) . i implies a is_applicable_to s )
assume A3: ( i in dom v2 & a = v2 . i & s = (apply v2,(v1 ast t)) . i ) ; :: thesis: a is_applicable_to s
A4: apply (v1 ^ v2),t = (apply v1,t) $^ (apply v2,(v1 ast t)) by Th35;
i >= 1 by A3, FINSEQ_3:27;
then consider j being Nat such that
A5: i = 1 + j by NAT_1:10;
i <= len v2 by A3, FINSEQ_3:27;
then ( len (apply v1,t) = (len v1) + 1 & len (apply v2,(v1 ast t)) = (len v2) + 1 & j < len v2 ) by A5, Def19, NAT_1:13;
then ( (len v1) + i = (len (apply v1,t)) + j & j < len (apply v2,(v1 ast t)) ) by A5, NAT_1:13;
then ( (len v1) + i in dom (v1 ^ v2) & a = (v1 ^ v2) . ((len v1) + i) & s = (apply (v1 ^ v2),t) . ((len v1) + i) ) by A3, A4, A5, Th34, FINSEQ_1:41, FINSEQ_1:def 7;
hence a is_applicable_to s by A1; :: thesis: verum