let T be non empty reflexive transitive non void TAS-structure ; 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; 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; ( 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
; ABCMIZ_0:def 28 ( 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
; ABCMIZ_0:def 28 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; ABCMIZ_0:def 28 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; 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; ( 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
; 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
;
a is_properly_applicable_to sthen
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;
verum end; end;