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:71;
[i,x] in q by A2, TARSKI:def 2;
then A4: i in dom q by RELAT_1:20;
[j,y] in q by A2, TARSKI:def 2;
then A5: j in dom q by RELAT_1:20;
A6: dom q = {i,j} by A2, RELAT_1:24;
ex k being Nat st dom q c= Seg k by FINSEQ_1:def 12;
then i >= 0 + 1 by A4, FINSEQ_1:3;
then Seq q = q * <*i,j*> by A1, A6, FINSEQ_3:51
.= <*(q . i),(q . j)*> by A4, A5, FINSEQ_2:145
.= <*x,(q . j)*> by A1, A3, FUNCT_4:66
.= <*x,y*> by A3, FUNCT_4:66 ;
hence Seq q = <*x,y*> ; :: thesis: verum