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 ^ p2

then (len p1) Shift p2 = {} by Th55;
hence (len p1) Shift p2 c= p1 ^ p2 by XBOOLE_1:2; :: thesis: verum

end;

suppose A1: p2 <> {} ; :: thesis: (len p1) Shift p2 c= p1 ^ p2

A2: dom ((len p1) Shift p2) = { ((len p1) + k) where k is Element of NAT : k in dom p2 } by Def15;
A3: dom ((len p1) Shift p2) = { k where k is Element of NAT : ( (len p1) + 1 <= k & k <= (len p1) + (len p2) ) } by A1, Th54;
A4: 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 b₁ being set holds
( not [x,b₁] in (len p1) Shift p2 or [x,b₁] in p1 ^ p2 )
let y be set ; :: thesis: ( not [x,y] in (len p1) Shift p2 or [x,y] in p1 ^ p2 )
assume [x,y] in (len p1) Shift p2 ; :: thesis: [x,y] in p1 ^ p2
then A5: ( x in dom ((len p1) Shift p2) & y = ((len p1) Shift p2) . x ) by FUNCT_1:8;
then consider k being Element of NAT such that
A6: ( x = k & (len p1) + 1 <= k & k <= (len p1) + (len p2) ) by A3;
1 <= (len p1) + 1 by INT_1:19;
then 1 <= k by A6, XXREAL_0:2;
then A7: x in dom (p1 ^ p2) by A4, A6;
consider j being Element of NAT such that
A8: ( x = (len p1) + j & j in dom p2 ) by A2, A5;
y = p2 . j by A5, A8, Def15
.= (p1 ^ p2) . x by A8, FINSEQ_1:def 7 ;
hence [x,y] in p1 ^ p2 by A7, FUNCT_1:8; :: thesis: verum

end;

end;