let n be Nat; :: thesis: for p being XFinSequence holds (p | n) ^ (p /^ n) = p
let p be XFinSequence; :: thesis: (p | n) ^ (p /^ n) = p
set pn = p /^ n;

now :: thesis: ( ( len p <= n & (p | n) ^ (p /^ n) = p ) or ( n < len p & (p | n) ^ (p /^ n) = p ) )

per cases ( len p <= n or n < len p ) ;

case A1: len p <= n ; :: thesis: (p | n) ^ (p /^ n) = p

p /^ n = {} by A1, Th6;
hence (p | n) ^ (p /^ n) = p by A1, AFINSQ_1:52; :: thesis: verum

end;

case A2: n < len p ; :: thesis: (p | n) ^ (p /^ n) = p

set g = p | n;
A3: len (p | n) = n by A2, AFINSQ_1:54;
A4: len (p /^ n) = (len p) - n by A2, Th7;

A5: now :: thesis: for m being Nat st m < len p holds
((p | n) ^ (p /^ n)) . m = p . m

let m be Nat; :: thesis: ( m < len p implies ((p | n) ^ (p /^ n)) . m = p . m )
assume A6: m < len p ; :: thesis: ((p | n) ^ (p /^ n)) . m = p . m

now :: thesis: ( ( m < n & ((p | n) ^ (p /^ n)) . m = p . m ) or ( n <= m & ((p | n) ^ (p /^ n)) . m = p . m ) )

per cases ( m < n or n <= m ) ;

case m < n ; :: thesis: ((p | n) ^ (p /^ n)) . m = p . m

then A7: m in Segm n by NAT_1:44;
hence ((p | n) ^ (p /^ n)) . m = (p | n) . m by A3, AFINSQ_1:def 3
.= p . m by A2, A7, AFINSQ_1:53 ;
:: thesis: verum

end;

case n <= m ; :: thesis: ((p | n) ^ (p /^ n)) . m = p . m

then max (0,(m - n)) = m - n by FINSEQ_2:4;
then reconsider k = m - n as Element of NAT by FINSEQ_2:5;
k < len (p /^ n) by A4, A6, XREAL_1:9;
then A8: k in dom (p /^ n) by AFINSQ_1:86;
m = (len (p | n)) + k by A3;
hence ((p | n) ^ (p /^ n)) . m = (p /^ n) . k by A8, AFINSQ_1:def 3
.= p . (k + n) by A8, Def2
.= p . m ;
:: thesis: verum

end;

end;

end;

hence ((p | n) ^ (p /^ n)) . m = p . m ; :: thesis: verum

end;

len ((p | n) ^ (p /^ n)) = n + ((len p) - n) by A4, A3, AFINSQ_1:17
.= len p ;
hence (p | n) ^ (p /^ n) = p by A5, AFINSQ_1:9; :: thesis: verum

end;

end;

end;

hence (p | n) ^ (p /^ n) = p ; :: thesis: verum