let p, q be FinSequence; :: thesis: for k, m being Element of NAT st k in dom p & m in dom q & m < k holds
m in dom p
let k, m be Element of NAT ; :: thesis: ( k in dom p & m in dom q & m < k implies m in dom p )
assume that
A1: k in dom p and
A2: m in dom q and
A3: m < k ; :: thesis: m in dom p
A4: dom p = Seg (len p) by FINSEQ_1:def 3;
A5: dom q = Seg (len q) by FINSEQ_1:def 3;
A6: 1 <= m by A2, A5, FINSEQ_1:1;
k <= len p by A1, A4, FINSEQ_1:1;
then m <= len p by A3, XXREAL_0:2;
hence m in dom p by A4, A6, FINSEQ_1:1; :: thesis: verum