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