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

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

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

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

end;

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

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

A6: now

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

now

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

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

then A8: m in n by NAT_1:44;
hence ((p | n) ^ (p /^ n)) . m = (p | n) . m by A4, AFINSQ_1:def 3
.= p . m by A3, A8, 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 A5, A7, XREAL_1:9;
then A9: k in dom (p /^ n) by NAT_1:44;
m = (len (p | n)) + k by A4;
hence ((p | n) ^ (p /^ n)) . m = (p /^ n) . k by A9, AFINSQ_1:def 3
.= p . (k + n) by A9, 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 A5, A4, AFINSQ_1:17
.= len p ;
hence (p | n) ^ (p /^ n) = p by A6, AFINSQ_1:9; :: thesis: verum

end;

end;

end;

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