let T be non empty reflexive transitive non void TA-structure ; for t being type of T
for v1, v2 being FinSequence of the adjectives of T holds apply ((v1 ^ v2),t) = (apply (v1,t)) $^ (apply (v2,(v1 ast t)))
let t be type of T; for v1, v2 being FinSequence of the adjectives of T holds apply ((v1 ^ v2),t) = (apply (v1,t)) $^ (apply (v2,(v1 ast t)))
let v1, v2 be FinSequence of the adjectives of T; apply ((v1 ^ v2),t) = (apply (v1,t)) $^ (apply (v2,(v1 ast t)))
consider tt being FinSequence of the carrier of T, q being Element of T such that
A1:
apply (v1,t) = tt ^ <*q*>
by HILBERT2:4;
set s = (apply (v1,t)) $^ (apply (v2,(v1 ast t)));
set p = v1 ^ v2;
A2:
len (apply (v1,t)) = (len v1) + 1
by Def19;
A3:
(apply (v1,t)) $^ (apply (v2,(v1 ast t))) = tt ^ (apply (v2,(v1 ast t)))
by A1, REWRITE1:2;
len <*q*> = 1
by FINSEQ_1:39;
then A4:
(len v1) + 1 = (len tt) + 1
by A2, A1, FINSEQ_1:22;
A5:
((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . 1 = t
proof
per cases
( len v1 = 0 or len v1 > 0 )
;
suppose
len v1 > 0
;
((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . 1 = tthen
len tt >= 0 + 1
by A4, NAT_1:13;
then A8:
1
in dom tt
by FINSEQ_3:25;
then A9:
tt . 1
= (apply (v1,t)) . 1
by A1, FINSEQ_1:def 7;
((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . 1
= tt . 1
by A3, A8, FINSEQ_1:def 7;
hence
((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . 1
= t
by A9, Def19;
verum end;
end;
A10:
now for i being Element of NAT
for a being adjective of T
for t9 being type of T st i in dom (v1 ^ v2) & a = (v1 ^ v2) . i & t9 = ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . i holds
((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . (i + 1) = a ast t9A11:
len (v1 ^ v2) = (len v1) + (len v2)
by FINSEQ_1:22;
A12:
len (apply (v2,(v1 ast t))) = (len v2) + 1
by Def19;
let i be
Element of
NAT ;
for a being adjective of T
for t9 being type of T st i in dom (v1 ^ v2) & a = (v1 ^ v2) . i & t9 = ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . i holds
((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . (b3 + 1) = b4 ast b5let a be
adjective of
T;
for t9 being type of T st i in dom (v1 ^ v2) & a = (v1 ^ v2) . i & t9 = ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . i holds
((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . (b2 + 1) = b3 ast b4let t9 be
type of
T;
( i in dom (v1 ^ v2) & a = (v1 ^ v2) . i & t9 = ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . i implies ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . (b1 + 1) = b2 ast b3 )assume that A13:
i in dom (v1 ^ v2)
and A14:
a = (v1 ^ v2) . i
and A15:
t9 = ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . i
;
((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . (b1 + 1) = b2 ast b3A16:
1
<= i
by A13, FINSEQ_3:25;
A17:
i <= len (v1 ^ v2)
by A13, FINSEQ_3:25;
per cases
( i < len v1 or i = len v1 or i > len v1 )
by XXREAL_0:1;
suppose A18:
i < len v1
;
((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . (b1 + 1) = b2 ast b3A19:
i + 1
>= 1
by NAT_1:11;
i + 1
<= len v1
by A18, NAT_1:13;
then A20:
i + 1
in dom tt
by A4, A19, FINSEQ_3:25;
then A21:
((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . (i + 1) = tt . (i + 1)
by A3, FINSEQ_1:def 7;
A22:
i in dom tt
by A4, A16, A18, FINSEQ_3:25;
then A23:
((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . i = tt . i
by A3, FINSEQ_1:def 7;
A24:
tt . (i + 1) = (apply (v1,t)) . (i + 1)
by A1, A20, FINSEQ_1:def 7;
A25:
tt . i = (apply (v1,t)) . i
by A1, A22, FINSEQ_1:def 7;
A26:
i in dom v1
by A16, A18, FINSEQ_3:25;
then
(v1 ^ v2) . i = v1 . i
by FINSEQ_1:def 7;
hence
((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . (i + 1) = a ast t9
by A14, A15, A26, A23, A25, A21, A24, Def19;
verum end; suppose A27:
i = len v1
;
((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . (b1 + 1) = b2 ast b3
1
<= len (apply (v2,(v1 ast t)))
by A12, NAT_1:11;
then
1
in dom (apply (v2,(v1 ast t)))
by FINSEQ_3:25;
then A28:
((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . (i + 1) = (apply (v2,(v1 ast t))) . 1
by A3, A4, A27, FINSEQ_1:def 7;
A29:
i in dom tt
by A4, A16, A27, FINSEQ_3:25;
then A30:
((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . i = tt . i
by A3, FINSEQ_1:def 7;
A31:
tt . i = (apply (v1,t)) . i
by A1, A29, FINSEQ_1:def 7;
A32:
i in dom v1
by A16, A27, FINSEQ_3:25;
then
(v1 ^ v2) . i = v1 . i
by FINSEQ_1:def 7;
then
a ast t9 = v1 ast t
by A14, A15, A27, A32, A30, A31, Def19;
hence
((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . (i + 1) = a ast t9
by A28, Def19;
verum suppose
i > len v1
;
((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . (b1 + 1) = b2 ast b3then
i >= (len v1) + 1
by NAT_1:13;
then consider j being
Nat such that A33:
i = ((len v1) + 1) + j
by NAT_1:10;
A34:
(1 + j) + 1
>= 1
by NAT_1:11;
A35:
((j + 1) + (len v1)) + 1
= ((j + 1) + 1) + (len v1)
;
A36:
1
+ j >= 1
by NAT_1:11;
A37:
i = (j + 1) + (len v1)
by A33;
then A38:
1
+ j <= len v2
by A17, A11, XREAL_1:6;
then
(1 + j) + 0 <= (len v2) + 1
by XREAL_1:7;
then
j + 1
in dom (apply (v2,(v1 ast t)))
by A12, A36, FINSEQ_3:25;
then A39:
((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . i = (apply (v2,(v1 ast t))) . (j + 1)
by A3, A4, A37, FINSEQ_1:def 7;
(1 + j) + 1
<= (len v2) + 1
by A38, XREAL_1:7;
then
(j + 1) + 1
in dom (apply (v2,(v1 ast t)))
by A12, A34, FINSEQ_3:25;
then A40:
((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . (i + 1) = (apply (v2,(v1 ast t))) . ((j + 1) + 1)
by A3, A4, A33, A35, FINSEQ_1:def 7;
A41:
j + 1
in dom v2
by A36, A38, FINSEQ_3:25;
then
(v1 ^ v2) . i = v2 . (j + 1)
by A37, FINSEQ_1:def 7;
hence
((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . (i + 1) = a ast t9
by A14, A15, A41, A39, A40, Def19;
verum end; end;
len (apply (v2,(v1 ast t))) = (len v2) + 1
by Def19;
then len ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) =
(len tt) + ((len v2) + 1)
by A3, FINSEQ_1:22
.=
((len v1) + (len v2)) + 1
by A4
.=
(len (v1 ^ v2)) + 1
by FINSEQ_1:22
;
hence
apply ((v1 ^ v2),t) = (apply (v1,t)) $^ (apply (v2,(v1 ast t)))
by A3, A5, A10, Def19; verum