let k be Nat; :: thesis: for p being FinSequence st not k in dom p holds
(p /^ k) ^ (p | k) = p
let p be FinSequence; :: thesis: ( not k in dom p implies (p /^ k) ^ (p | k) = p )
assume not k in dom p ; :: thesis: (p /^ k) ^ (p | k) = p

per cases then ( k < 1 or k > len p ) by FINSEQ_3:25;

suppose k < 1 ; :: thesis: (p /^ k) ^ (p | k) = p

then k = 0 by NAT_1:14;
then ( p | k = {} & p /^ k = p ) by FINSEQ_5:28;
hence (p /^ k) ^ (p | k) = p by FINSEQ_1:34; :: thesis: verum

end;

suppose k > len p ; :: thesis: (p /^ k) ^ (p | k) = p

then ( p /^ k = {} & p | k = p ) by RFINSEQ:def 1, FINSEQ_1:58;
hence (p /^ k) ^ (p | k) = p by FINSEQ_1:34; :: thesis: verum

end;

end;