let i, j be Nat; :: thesis: for x, y being set
for q being FinSubsequence st i < j & q = {[i,x],[j,y]} holds
Seq q = <*x,y*>
let x, y be set ; :: thesis: for q being FinSubsequence st i < j & q = {[i,x],[j,y]} holds
Seq q = <*x,y*>
let q be FinSubsequence; :: thesis: ( i < j & q = {[i,x],[j,y]} implies Seq q = <*x,y*> )
assume that
A1: i < j and
A2: q = {[i,x],[j,y]} ; :: thesis: Seq q = <*x,y*>
A3: q = (i,j) --> (x,y) by A1, A2, FUNCT_4:67;
[i,x] in q by A2, TARSKI:def 2;
then A4: i in dom q by XTUPLE_0:def 12;
[j,y] in q by A2, TARSKI:def 2;
then A5: j in dom q by XTUPLE_0:def 12;
A6: dom q = {i,j} by A2, RELAT_1:10;
ex k being Nat st dom q c= Seg k by FINSEQ_1:def 12;
then i >= 0 + 1 by A4, FINSEQ_1:1;
then Seq q = q * <*i,j*> by A1, A6, FINSEQ_3:45
.= <*(q . i),(q . j)*> by A4, A5, FINSEQ_2:125
.= <*x,(q . j)*> by A1, A3, FUNCT_4:63
.= <*x,y*> by A3, FUNCT_4:63 ;
hence Seq q = <*x,y*> ; :: thesis: verum