let T be non empty reflexive transitive non void TAS-structure ; :: thesis: for t being type of T
for v1, v2 being FinSequence of the adjectives of T st v1 is_properly_applicable_to t & v2 is_properly_applicable_to v1 ast t holds
v1 ^ v2 is_properly_applicable_to t
let t be type of T; :: thesis: for v1, v2 being FinSequence of the adjectives of T st v1 is_properly_applicable_to t & v2 is_properly_applicable_to v1 ast t holds
v1 ^ v2 is_properly_applicable_to t
let v1, v2 be FinSequence of the adjectives of T; :: thesis: ( v1 is_properly_applicable_to t & v2 is_properly_applicable_to v1 ast t implies v1 ^ v2 is_properly_applicable_to 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 & a = v1 . i & s = (apply v1,t) . i holds
a is_properly_applicable_to s ; :: according to ABCMIZ_0:def 28 :: thesis: ( not v2 is_properly_applicable_to v1 ast t or v1 ^ v2 is_properly_applicable_to t )
assume A2: for i being natural number
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_properly_applicable_to s ; :: according to ABCMIZ_0:def 28 :: thesis: v1 ^ v2 is_properly_applicable_to t
let i be natural number ; :: according to ABCMIZ_0:def 28 :: thesis: 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_properly_applicable_to s
let a be adjective of T; :: thesis: 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_properly_applicable_to s
let s be type of T; :: thesis: ( i in dom (v1 ^ v2) & a = (v1 ^ v2) . i & s = (apply (v1 ^ v2),t) . i implies a is_properly_applicable_to s )
assume A3: ( i in dom (v1 ^ v2) & a = (v1 ^ v2) . i & s = (apply (v1 ^ v2),t) . i ) ; :: thesis: a is_properly_applicable_to s
A4: apply (v1 ^ v2),t = (apply v1,t) $^ (apply v2,(v1 ast t)) by Th35;
A5: ( i >= 1 & i <= len (v1 ^ v2) & i is Element of NAT ) by A3, FINSEQ_3:27;

per cases ( i <= len v1 or i > len v1 ) ;

suppose i <= len v1 ; :: thesis: a is_properly_applicable_to s

then A6: i in dom v1 by A5, FINSEQ_3:27;
then ( a = v1 . i & s = (apply v1,t) . i ) by A3, Th36, FINSEQ_1:def 7;
hence a is_properly_applicable_to s by A1, A6; :: thesis: verum

end;

suppose i > len v1 ; :: thesis: a is_properly_applicable_to s

then i >= 1 + (len v1) by NAT_1:13;
then consider j being Nat such that
A7: i = ((len v1) + 1) + j by NAT_1:10;
( len (v1 ^ v2) = (len v1) + (len v2) & i = (len v1) + (j + 1) ) by A7, FINSEQ_1:35;
then ( j + 1 >= 1 & j + 1 <= len v2 ) by A5, NAT_1:11, XREAL_1:8;
then A8: ( len (apply v1,t) = (len v1) + 1 & len (apply v2,(v1 ast t)) = (len v2) + 1 & j < len v2 & j + 1 in dom v2 ) by Def19, FINSEQ_3:27, NAT_1:13;
then ( (len v1) + (j + 1) = (len (apply v1,t)) + j & j < len (apply v2,(v1 ast t)) ) by NAT_1:13;
then ( a = v2 . (1 + j) & s = (apply v2,(v1 ast t)) . (1 + j) ) by A3, A4, A7, A8, Th34, FINSEQ_1:def 7;
hence a is_properly_applicable_to s by A2, A8; :: thesis: verum

end;

end;