let i be Nat; :: thesis: for p, q being FinSequence st i <= len p holds
(p ^ q) | (Seg i) = p | (Seg i)
let p, q be FinSequence; :: thesis: ( i <= len p implies (p ^ q) | (Seg i) = p | (Seg i) )
set D = ((rng p) \/ (rng q)) \/ {0};
( rng p c= (rng p) \/ (rng q) & rng q c= (rng p) \/ (rng q) ) by XBOOLE_1:7;
then ( p is FinSequence of ((rng p) \/ (rng q)) \/ {0} & q is FinSequence of ((rng p) \/ (rng q)) \/ {0} & (p ^ q) | i = (p ^ q) | (Seg i) & p | (Seg i) = p | i ) by FINSEQ_1:def 4, XBOOLE_1:10;
hence ( i <= len p implies (p ^ q) | (Seg i) = p | (Seg i) ) by FINSEQ_5:22; :: thesis: verum