let T be non empty reflexive transitive non void TA-structure ; :: thesis: 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; :: thesis: 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; :: thesis: apply (v1 ^ v2),t = (apply v1,t) $^ (apply v2,(v1 ast t))
A1: ( len (apply v1,t) = (len v1) + 1 & len (apply v2,(v1 ast t)) = (len v2) + 1 ) by Def19;
consider tt being FinSequence of the carrier of T, q being Element of T such that
A2: apply v1,t = tt ^ <*q*> by HILBERT2:4;
A3: (apply v1,t) $^ (apply v2,(v1 ast t)) = tt ^ (apply v2,(v1 ast t)) by A2, REWRITE1:2;
len <*q*> = 1 by FINSEQ_1:56;
then A4: (len v1) + 1 = (len tt) + 1 by A1, A2, FINSEQ_1:35;
set s = (apply v1,t) $^ (apply v2,(v1 ast t));
set p = v1 ^ v2;
A5: len ((apply v1,t) $^ (apply v2,(v1 ast t))) = (len tt) + ((len v2) + 1) by A1, A3, FINSEQ_1:35
.= ((len v1) + (len v2)) + 1 by A4
.= (len (v1 ^ v2)) + 1 by FINSEQ_1:35 ;
A6: ((apply v1,t) $^ (apply v2,(v1 ast t))) . 1 = t

proof

per cases ( len v1 = 0 or len v1 > 0 ) ;

suppose len v1 = 0 ; :: thesis: ((apply v1,t) $^ (apply v2,(v1 ast t))) . 1 = t

then ( v1 = <*> the adjectives of T & tt = {} ) by A4;
then ( (apply v1,t) $^ (apply v2,(v1 ast t)) = apply v2,(v1 ast t) & v1 ast t = t ) by A3, Def19, CARD_1:47, FINSEQ_1:47;
hence ((apply v1,t) $^ (apply v2,(v1 ast t))) . 1 = t by Def19; :: thesis: verum

end;

suppose len v1 > 0 ; :: thesis: ((apply v1,t) $^ (apply v2,(v1 ast t))) . 1 = t

then ( len tt >= 0 + 1 & 0 + 1 = 1 & 1 <= 1 ) by A4, NAT_1:13;
then 1 in dom tt by FINSEQ_3:27;
then ( ((apply v1,t) $^ (apply v2,(v1 ast t))) . 1 = tt . 1 & tt . 1 = (apply v1,t) . 1 ) by A2, A3, FINSEQ_1:def 7;
hence ((apply v1,t) $^ (apply v2,(v1 ast t))) . 1 = t by Def19; :: thesis: verum

end;

end;

end;

now

let i be Element of NAT ; :: thesis: for a being adjective of T
for t' being type of T st i in dom (v1 ^ v2) & a = (v1 ^ v2) . i & t' = ((apply v1,t) $^ (apply v2,(v1 ast t))) . i holds
((apply v1,t) $^ (apply v2,(v1 ast t))) . (b₃ + 1) = b₄ ast b₅
let a be adjective of T; :: thesis: for t' being type of T st i in dom (v1 ^ v2) & a = (v1 ^ v2) . i & t' = ((apply v1,t) $^ (apply v2,(v1 ast t))) . i holds
((apply v1,t) $^ (apply v2,(v1 ast t))) . (b₂ + 1) = b₃ ast b₄
let t' be type of T; :: thesis: ( i in dom (v1 ^ v2) & a = (v1 ^ v2) . i & t' = ((apply v1,t) $^ (apply v2,(v1 ast t))) . i implies ((apply v1,t) $^ (apply v2,(v1 ast t))) . (b₁ + 1) = b₂ ast b₃ )
assume that
A7: i in dom (v1 ^ v2) and
A8: ( a = (v1 ^ v2) . i & t' = ((apply v1,t) $^ (apply v2,(v1 ast t))) . i ) ; :: thesis: ((apply v1,t) $^ (apply v2,(v1 ast t))) . (b₁ + 1) = b₂ ast b₃
A9: ( 1 <= i & i <= len (v1 ^ v2) & len (v1 ^ v2) = (len v1) + (len v2) ) by A7, FINSEQ_1:35, FINSEQ_3:27;
A10: len (apply v2,(v1 ast t)) = (len v2) + 1 by Def19;

per cases ( i < len v1 or i = len v1 or i > len v1 ) by XXREAL_0:1;

suppose i < len v1 ; :: thesis: ((apply v1,t) $^ (apply v2,(v1 ast t))) . (b₁ + 1) = b₂ ast b₃

then ( i + 1 <= len v1 & i <= len v1 & i + 1 >= 1 ) by NAT_1:11, NAT_1:13;
then A11: ( i in dom tt & i + 1 in dom tt & i in dom v1 ) by A4, A9, FINSEQ_3:27;
then ( ((apply v1,t) $^ (apply v2,(v1 ast t))) . i = tt . i & tt . i = (apply v1,t) . i & ((apply v1,t) $^ (apply v2,(v1 ast t))) . (i + 1) = tt . (i + 1) & (v1 ^ v2) . i = v1 . i & tt . (i + 1) = (apply v1,t) . (i + 1) ) by A2, A3, FINSEQ_1:def 7;
hence ((apply v1,t) $^ (apply v2,(v1 ast t))) . (i + 1) = a ast t' by A8, A11, Def19; :: thesis: verum

end;

suppose A12: i = len v1 ; :: thesis: ((apply v1,t) $^ (apply v2,(v1 ast t))) . (b₁ + 1) = b₂ ast b₃

1 <= len (apply v2,(v1 ast t)) by A10, NAT_1:11;
then A13: ( i in dom tt & i in dom v1 & 1 in dom (apply v2,(v1 ast t)) ) by A4, A9, A12, FINSEQ_3:27;
then A14: ( ((apply v1,t) $^ (apply v2,(v1 ast t))) . i = tt . i & tt . i = (apply v1,t) . i & ((apply v1,t) $^ (apply v2,(v1 ast t))) . (i + 1) = (apply v2,(v1 ast t)) . 1 & (v1 ^ v2) . i = v1 . i ) by A2, A3, A4, A12, FINSEQ_1:def 7;
then a ast t' = v1 ast t by A8, A12, A13, Def19;
hence ((apply v1,t) $^ (apply v2,(v1 ast t))) . (i + 1) = a ast t' by A14, Def19; :: thesis: verum

end;

suppose i > len v1 ; :: thesis: ((apply v1,t) $^ (apply v2,(v1 ast t))) . (b₁ + 1) = b₂ ast b₃

then i >= (len v1) + 1 by NAT_1:13;
then consider j being Nat such that
A15: i = ((len v1) + 1) + j by NAT_1:10;
A16: ( i = (j + 1) + (len v1) & ((j + 1) + (len v1)) + 1 = ((j + 1) + 1) + (len v1) ) by A15;
then A17: ( 1 + j >= 1 & 1 + j <= len v2 & 0 <= 1 ) by A9, NAT_1:11, XREAL_1:8;
then ( (1 + j) + 1 <= (len v2) + 1 & (1 + j) + 1 >= 1 & (1 + j) + 0 <= (len v2) + 1 ) by NAT_1:11, XREAL_1:9;
then A18: ( j + 1 in dom v2 & j + 1 in dom (apply v2,(v1 ast t)) & (j + 1) + 1 in dom (apply v2,(v1 ast t)) ) by A10, A17, FINSEQ_3:27;
then ( ((apply v1,t) $^ (apply v2,(v1 ast t))) . i = (apply v2,(v1 ast t)) . (j + 1) & (v1 ^ v2) . i = v2 . (j + 1) & ((apply v1,t) $^ (apply v2,(v1 ast t))) . (i + 1) = (apply v2,(v1 ast t)) . ((j + 1) + 1) ) by A3, A4, A16, FINSEQ_1:def 7;
hence ((apply v1,t) $^ (apply v2,(v1 ast t))) . (i + 1) = a ast t' by A8, A18, Def19; :: thesis: verum

end;

end;

end;

hence apply (v1 ^ v2),t = (apply v1,t) $^ (apply v2,(v1 ast t)) by A3, A5, A6, Def19; :: thesis: verum