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 ^ v2 is_properly_applicable_to t holds
( v1 is_properly_applicable_to t & v2 is_properly_applicable_to v1 ast t )
let t be type of T; for v1, v2 being FinSequence of the adjectives of T st v1 ^ v2 is_properly_applicable_to t holds
( v1 is_properly_applicable_to t & v2 is_properly_applicable_to v1 ast t )
let v1, v2 be FinSequence of the adjectives of T; ( v1 ^ v2 is_properly_applicable_to t implies ( v1 is_properly_applicable_to t & v2 is_properly_applicable_to v1 ast t ) )
set v = v1 ^ v2;
A1:
apply ((v1 ^ v2),t) = (apply (v1,t)) $^ (apply (v2,(v1 ast t)))
by Th34;
A2:
len (apply (v2,(v1 ast t))) = (len v2) + 1
by Def19;
assume A3:
for i being Nat
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
; ABCMIZ_0:def 28 ( v1 is_properly_applicable_to t & v2 is_properly_applicable_to v1 ast t )
hereby ABCMIZ_0:def 28 v2 is_properly_applicable_to v1 ast t
A4:
dom v1 c= dom (v1 ^ v2)
by FINSEQ_1:26;
let i be
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 slet a be
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 slet s be
type of
T;
( i in dom v1 & a = v1 . i & s = (apply (v1,t)) . i implies a is_properly_applicable_to s )assume that A5:
i in dom v1
and A6:
a = v1 . i
and A7:
s = (apply (v1,t)) . i
;
a is_properly_applicable_to sA8:
a = (v1 ^ v2) . i
by A5, A6, FINSEQ_1:def 7;
s = (apply ((v1 ^ v2),t)) . i
by A5, A7, Th35;
hence
a is_properly_applicable_to s
by A3, A5, A4, A8;
verum
end;
let i be Nat; ABCMIZ_0:def 28 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
let a be 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
let s be type of T; ( i in dom v2 & a = v2 . i & s = (apply (v2,(v1 ast t))) . i implies a is_properly_applicable_to s )
assume that
A9:
i in dom v2
and
A10:
a = v2 . i
and
A11:
s = (apply (v2,(v1 ast t))) . i
; a is_properly_applicable_to s
A12:
a = (v1 ^ v2) . ((len v1) + i)
by A9, A10, FINSEQ_1:def 7;
i >= 1
by A9, FINSEQ_3:25;
then consider j being Nat such that
A13:
i = 1 + j
by NAT_1:10;
i <= len v2
by A9, FINSEQ_3:25;
then
j < len v2
by A13, NAT_1:13;
then A14:
j < len (apply (v2,(v1 ast t)))
by A2, NAT_1:13;
len (apply (v1,t)) = (len v1) + 1
by Def19;
then
(len v1) + i = (len (apply (v1,t))) + j
by A13;
then
s = (apply ((v1 ^ v2),t)) . ((len v1) + i)
by A11, A1, A13, A14, Th33;
hence
a is_properly_applicable_to s
by A3, A9, A12, FINSEQ_1:28; verum