let x be object ; :: thesis: for p, q being FinSequence st x in dom q holds
ex k being Nat st
( k = x & (len p) + k in dom (p ^ q) )
let p, q be FinSequence; :: 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 A2: x in Seg (len q) by Def3;
reconsider k = x as Element of NAT by A1;
take k ; :: thesis: ( k = x & (len p) + k in dom (p ^ q) )
A3: 1 <= k by A2, Th1;
A4: k <= len q by A2, Th1;
k <= (len p) + k by NAT_1:11;
then A5: 1 <= (len p) + k by A3, XXREAL_0:2;
(len p) + k <= (len p) + (len q) by A4, XREAL_1:7;
then (len p) + k in Seg ((len p) + (len q)) by A5;
hence ( k = x & (len p) + k in dom (p ^ q) ) by Def7; :: thesis: verum