let p, q be FinSequence; ( 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))
; FUNCT_7:def 8 ( 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:19;
A3:
len (p ^ q) = (len p) + (len q)
by FINSEQ_1:35;
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:21;
hereby FUNCT_7:def 8 q is FuncSeq-like
take p1 =
p1;
( 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 A6:
len p1 = (len p) + 1
by FINSEQ_1:21;
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 ;
( i in dom p implies p . i in Funcs (p1 . i),(p1 . (i + 1)) )assume A7:
i in dom p
;
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:24;
i in dom p1
by A6, A7, Th24;
then A9:
pq . i = p1 . i
by FUNCT_1:70;
i + 1
in dom p1
by A6, A7, Th24;
hence
p . i in Funcs (p1 . i),
(p1 . (i + 1))
by A8, A9, FUNCT_1:70;
verum
end;
consider q2 being FinSequence such that
A10:
pq = p2 ^ q2
by FINSEQ_1:101;
take
q2
; FUNCT_7:def 8 ( 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 pq = (len p2) + (len q2)
by A10, FINSEQ_1:35;
hence
len q2 = (len q) + 1
by A1, A3, A5; 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 ; ( x in dom q implies q . x in Funcs (q2 . x),(q2 . (x + 1)) )
assume A11:
x in dom q
; 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:41;
A13:
(len p) + ((len q) + 1) = (len p) + (len q2)
by A1, A3, A10, A5, FINSEQ_1:35;
then
x + 1 in dom q2
by A11, Th24;
then A14:
q2 . (x + 1) = pq . ((len p) + (x + 1))
by A10, A5, FINSEQ_1:def 7;
x in dom q2
by A13, A11, Th24;
hence
q . x in Funcs (q2 . x),(q2 . (x + 1))
by A10, A5, A12, A14, FINSEQ_1:def 7; verum