let i, j be Nat; :: thesis: for x, y being set st 0 < i & i < j holds
{[i,x],[j,y]} is FinSubsequence
let x, y be set ; :: thesis: ( 0 < i & i < j implies {[i,x],[j,y]} is FinSubsequence )
assume that
A1: 0 < i and
A2: i < j ; :: thesis: {[i,x],[j,y]} is FinSubsequence
reconsider X = {[i,x],[j,y]} as Function by A2, GRFUNC_1:8;
A3: 0 + 1 <= i by A1, NAT_1:13;
now :: thesis: for x being object st x in {i,j} holds
x in Seg j
let x be object ; :: thesis: ( x in {i,j} implies x in Seg j )
assume x in {i,j} ; :: thesis: x in Seg j
then A4: ( x = i or x = j ) by TARSKI:def 2;
thus x in Seg j by A2, A3, A4, FINSEQ_1:3; :: thesis: verum
end;
then ( dom X = {i,j} & {i,j} c= Seg j ) by RELAT_1:10;
hence {[i,x],[j,y]} is FinSubsequence by FINSEQ_1:def 12; :: thesis: verum