let n be Nat; :: thesis: for p, q being XFinSequence st n < len p holds
(p ^ q) . n = p . n
let p, q be XFinSequence; :: thesis: ( n < len p implies (p ^ q) . n = p . n )
assume n < len p ; :: thesis: (p ^ q) . n = p . n
then n in dom p by Lm1;
hence (p ^ q) . n = p . n by Def3; :: thesis: verum