let p, q be FinSequence; :: thesis: ( p ^ q is FuncSeq-like implies ( p is FuncSeq-like & q is FuncSeq-like ) )
given pq being FinSequence such that A1: len pq = (len (p ^ q)) + 1 and
A2: for i being Element of NAT st i in dom (p ^ q) holds
(p ^ q) . i in Funcs (pq . i),(pq . (i + 1)) ; :: according to FUNCT_7:def 8 :: thesis: ( p is FuncSeq-like & q is FuncSeq-like )
A3: len (p ^ q) = (len p) + (len q) by FINSEQ_1:35;
reconsider p1 = pq | (Seg ((len p) + 1)), p2 = pq | (Seg (len p)) as FinSequence by FINSEQ_1:19;

hereby :: according to FUNCT_7:def 8 :: thesis: q is FuncSeq-like

take p1 = p1; :: thesis: ( len p1 = (len p) + 1 & ( for i being Element of NAT st i in dom p holds
p . i in Funcs (p1 . i),(p1 . (i + 1)) ) )
len p <= len (p ^ q) by A3, NAT_1:11;
then (len p) + 1 <= len pq by A1, XREAL_1:8;
hence A4: len p1 = (len p) + 1 by FINSEQ_1:21; :: thesis: for i being Element of NAT st i in dom p holds
p . i in Funcs (p1 . i),(p1 . (i + 1))
let i be Element of NAT ; :: thesis: ( i in dom p implies p . i in Funcs (p1 . i),(p1 . (i + 1)) )
assume i in dom p ; :: thesis: p . i in Funcs (p1 . i),(p1 . (i + 1))
then ( (p ^ q) . i = p . i & i in dom (p ^ q) & i in dom p1 & i + 1 in dom p1 ) by A4, Th24, FINSEQ_1:def 7, FINSEQ_3:24;
then ( p . i in Funcs (pq . i),(pq . (i + 1)) & pq . i = p1 . i & pq . (i + 1) = p1 . (i + 1) ) by A2, FUNCT_1:70;
hence p . i in Funcs (p1 . i),(p1 . (i + 1)) ; :: thesis: verum

end;

consider q2 being FinSequence such that
A5: pq = p2 ^ q2 by TREES_1:3;
take q2 ; :: according to FUNCT_7:def 8 :: thesis: ( len q2 = (len q) + 1 & ( for i being Element of NAT st i in dom q holds
q . i in Funcs (q2 . i),(q2 . (i + 1)) ) )
( len p <= len (p ^ q) & len (p ^ q) <= len pq ) by A1, A3, NAT_1:11;
then len p <= len pq by XXREAL_0:2;
then A6: ( len p2 = len p & len pq = (len p2) + (len q2) ) by A5, FINSEQ_1:21, FINSEQ_1:35;
then A7: (len p) + ((len q) + 1) = (len p) + (len q2) by A1, A3;
thus len q2 = (len q) + 1 by A1, A3, A6; :: thesis: for i being Element of NAT st i in dom q holds
q . i in Funcs (q2 . i),(q2 . (i + 1))
let x be Element of NAT ; :: thesis: ( x in dom q implies q . x in Funcs (q2 . x),(q2 . (x + 1)) )
assume x in dom q ; :: thesis: q . x in Funcs (q2 . x),(q2 . (x + 1))
then ( (p ^ q) . ((len p) + x) = q . x & x in dom q2 & x + 1 in dom q2 & (len p) + x in dom (p ^ q) ) by A7, Th24, FINSEQ_1:41, FINSEQ_1:def 7;
then ( q . x in Funcs (pq . ((len p) + x)),(pq . (((len p) + x) + 1)) & q2 . x = pq . ((len p) + x) & q2 . (x + 1) = pq . ((len p) + (x + 1)) ) by A2, A5, A6, FINSEQ_1:def 7;
hence q . x in Funcs (q2 . x),(q2 . (x + 1)) ; :: thesis: verum