let p1, p2 be FinSequence; Shift (p2,(len p1)) c= p1 ^ p2
A1:
dom (Shift (p2,(len p1))) = { (k + (len p1)) where k is Nat : k in dom p2 }
by Def12;
A2:
dom (Shift (p2,(len p1))) = { k where k is Nat : ( (len p1) + 1 <= k & k <= (len p1) + (len p2) ) }
by Th39;
A3: dom (p1 ^ p2) =
Seg ((len p1) + (len p2))
by FINSEQ_1:def 7
.=
{ k where k is Nat : ( 1 <= k & k <= (len p1) + (len p2) ) }
;
let x, y be object ; RELAT_1:def 3 ( not [x,y] in Shift (p2,(len p1)) or [x,y] in p1 ^ p2 )
assume A4:
[x,y] in Shift (p2,(len p1))
; [x,y] in p1 ^ p2
then A5:
x in dom (Shift (p2,(len p1)))
by FUNCT_1:1;
A6:
y = (Shift (p2,(len p1))) . x
by A4, FUNCT_1:1;
consider k being 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:6;
then
1 <= k
by A8, XXREAL_0:2;
then A10:
x in dom (p1 ^ p2)
by A3, A7, A9;
consider j being Nat such that
A11:
x = j + (len p1)
and
A12:
j in dom p2
by A1, A5;
y =
p2 . j
by A6, A11, A12, Def12
.=
(p1 ^ p2) . x
by A11, A12, FINSEQ_1:def 7
;
hence
[x,y] in p1 ^ p2
by A10, FUNCT_1:1; verum