let x be set ; :: thesis: for q, p being XFinSequence st x in dom q holds
ex k being Nat st
( k = x & (len p) + k in dom (p ^ q) )
let q, p be XFinSequence; :: thesis: ( x in dom q implies ex k being Nat st
( k = x & (len p) + k in dom (p ^ q) ) )
assume A1: x in dom q ; :: thesis: ex k being Nat st
( k = x & (len p) + k in dom (p ^ q) )
then reconsider k = x as Element of NAT ;
take k ; :: thesis: ( k = x & (len p) + k in dom (p ^ q) )
k < len q by A1, NAT_1:45;
then (len p) + k < (len p) + (len q) by XREAL_1:10;
then (len p) + k in (len p) + (len q) by NAT_1:45;
hence ( k = x & (len p) + k in dom (p ^ q) ) by Def4; :: thesis: verum