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 Nat
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 Nat
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
A3: apply ((v1 ^ v2),t) = (apply (v1,t)) $^ (apply (v2,(v1 ast t))) by Th34;
let i be Nat; :: 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 that
A4: i in dom (v1 ^ v2) and
A5: a = (v1 ^ v2) . i and
A6: s = (apply ((v1 ^ v2),t)) . i ; :: thesis: a is_properly_applicable_to s
A7: i >= 1 by A4, FINSEQ_3:25;
A8: i <= len (v1 ^ v2) by A4, FINSEQ_3:25;

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

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

then A9: i in dom v1 by A7, FINSEQ_3:25;
then A10: a = v1 . i by A5, FINSEQ_1:def 7;
s = (apply (v1,t)) . i by A6, A9, Th35;
hence a is_properly_applicable_to s by A1, A9, A10; :: 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
A11: i = ((len v1) + 1) + j by NAT_1:10;
A12: len (apply (v2,(v1 ast t))) = (len v2) + 1 by Def19;
A13: len (v1 ^ v2) = (len v1) + (len v2) by FINSEQ_1:22;
A14: len (apply (v1,t)) = (len v1) + 1 by Def19;
i = (len v1) + (j + 1) by A11;
then A15: j + 1 <= len v2 by A8, A13, XREAL_1:6;
then j < len v2 by NAT_1:13;
then j < len (apply (v2,(v1 ast t))) by A12, NAT_1:13;
then A16: s = (apply (v2,(v1 ast t))) . (1 + j) by A6, A3, A11, A14, Th33;
j + 1 >= 1 by NAT_1:11;
then A17: j + 1 in dom v2 by A15, FINSEQ_3:25;
(len v1) + (j + 1) = (len (apply (v1,t))) + j by A14;
then a = v2 . (1 + j) by A5, A11, A17, FINSEQ_1:def 7;
hence a is_properly_applicable_to s by A2, A17, A16; :: thesis: verum

end;

end;