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 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 )
reconsider p1 = pq | (Seg ((len p) + 1)), p2 = pq | (Seg (len p)) as FinSequence by FINSEQ_1:15;
A3: len (p ^ q) = (len p) + (len q) by FINSEQ_1:22;
then A4: len p <= len (p ^ q) by NAT_1:11;
len (p ^ q) <= len pq by A1, NAT_1:11;
then len p <= len pq by A4, XXREAL_0:2;
then A5: len p2 = len p by FINSEQ_1:17;

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

take p1 = p1; :: thesis: ( len p1 = (len p) + 1 & ( for i being 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:6;
hence A6: len p1 = (len p) + 1 by FINSEQ_1:17; :: thesis: for i being Nat st i in dom p holds
p . i in Funcs ((p1 . i),(p1 . (i + 1)))
let i be Nat; :: thesis: ( i in dom p implies p . i in Funcs ((p1 . i),(p1 . (i + 1))) )
assume A7: i in dom p ; :: thesis: p . i in Funcs ((p1 . i),(p1 . (i + 1)))
then (p ^ q) . i = p . i by FINSEQ_1:def 7;
then A8: p . i in Funcs ((pq . i),(pq . (i + 1))) by A2, A7, FINSEQ_3:22;
i in dom p1 by A6, A7, Th22;
then A9: pq . i = p1 . i by FUNCT_1:47;
i + 1 in dom p1 by A6, A7, Th22;
hence p . i in Funcs ((p1 . i),(p1 . (i + 1))) by A8, A9, FUNCT_1:47; :: thesis: verum

end;

consider q2 being FinSequence such that
A10: pq = p2 ^ q2 by FINSEQ_1:80;
take q2 ; :: according to FUNCT_7:def 8 :: thesis: ( len q2 = (len q) + 1 & ( for i being Nat st i in dom q holds
q . i in Funcs ((q2 . i),(q2 . (i + 1))) ) )
len pq = (len p2) + (len q2) by A10, FINSEQ_1:22;
hence len q2 = (len q) + 1 by A1, A3, A5; :: thesis: for i being Nat st i in dom q holds
q . i in Funcs ((q2 . i),(q2 . (i + 1)))
let x be Nat; :: thesis: ( x in dom q implies q . x in Funcs ((q2 . x),(q2 . (x + 1))) )
assume A11: x in dom q ; :: thesis: q . x in Funcs ((q2 . x),(q2 . (x + 1)))
then (p ^ q) . ((len p) + x) = q . x by FINSEQ_1:def 7;
then A12: q . x in Funcs ((pq . ((len p) + x)),(pq . (((len p) + x) + 1))) by A2, A11, FINSEQ_1:28;
A13: (len p) + ((len q) + 1) = (len p) + (len q2) by A1, A3, A10, A5, FINSEQ_1:22;
then x + 1 in dom q2 by A11, Th22;
then A14: q2 . (x + 1) = pq . ((len p) + (x + 1)) by A10, A5, FINSEQ_1:def 7;
x in dom q2 by A13, A11, Th22;
hence q . x in Funcs ((q2 . x),(q2 . (x + 1))) by A10, A5, A12, A14, FINSEQ_1:def 7; :: thesis: verum