let p1, p2 be FinSequence; :: thesis: (len p1) Shift p2 c= p1 ^ p2
per cases
( p2 = {} or p2 <> {} )
;
suppose
p2 <> {}
;
:: thesis: (len p1) Shift p2 c= p1 ^ p2A1:
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 ;
:: according to RELAT_1:def 3 :: thesis: for b1 being set holds
( not [x,b1] in (len p1) Shift p2 or [x,b1] in p1 ^ p2 )let y be
set ;
:: thesis: ( not [x,y] in (len p1) Shift p2 or [x,y] in p1 ^ p2 )assume A4:
[x,y] in (len p1) Shift p2
;
:: thesis: [x,y] in p1 ^ p2then 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;
:: thesis: verum end;