let p1, p2 be FinSequence; (len p1) Shift p2 c= p1 ^ p2
A1:
dom ((len p1) Shift p2) = { ((len p1) + k) where k is Element of NAT : k in dom p2 }
by Def15;
A2:
dom ((len p1) Shift p2) = { k where k is Element of NAT : ( (len p1) + 1 <= k & k <= (len p1) + (len p2) ) }
by Th54;
A3: dom (p1 ^ p2) =
Seg ((len p1) + (len p2))
by FINSEQ_1:def 7
.=
{ k where k is Element of NAT : ( 1 <= k & k <= (len p1) + (len p2) ) }
by FINSEQ_1:def 1
;
let x be set ; RELAT_1:def 3 for b1 being set holds
( not [x,b1] in (len p1) Shift p2 or [x,b1] in p1 ^ p2 )
let y be set ; ( not [x,y] in (len p1) Shift p2 or [x,y] in p1 ^ p2 )
assume A4:
[x,y] in (len p1) Shift p2
; [x,y] in p1 ^ p2
then A5:
x in dom ((len p1) Shift p2)
by FUNCT_1:8;
A6:
y = ((len p1) Shift p2) . x
by A4, FUNCT_1:8;
consider k being Element of NAT such that
A7:
x = k
and
A8:
(len p1) + 1 <= k
and
A9:
k <= (len p1) + (len p2)
by A2, A5;
1 <= (len p1) + 1
by INT_1:19;
then
1 <= k
by A8, XXREAL_0:2;
then A10:
x in dom (p1 ^ p2)
by A3, A7, A9;
consider j being Element of NAT such that
A11:
x = (len p1) + j
and
A12:
j in dom p2
by A1, A5;
y =
p2 . j
by A6, A11, A12, Def15
.=
(p1 ^ p2) . x
by A11, A12, FINSEQ_1:def 7
;
hence
[x,y] in p1 ^ p2
by A10, FUNCT_1:8; verum