let n, m be natural number ; :: thesis: ( 0 < n & n < m implies Sgm {n,m} = <*n,m*> )
assume that
A1: 0 < n and
A2: n < m ; :: thesis: Sgm {n,m} = <*n,m*>
( Seg n c= Seg m & m in Seg m & n in Seg n ) by A1, A2, FINSEQ_1:5, FINSEQ_1:7;
then A3: {n,m} c= Seg m by ZFMISC_1:38;
then A4: len (Sgm {n,m}) = card {n,m} by Th44
.= 2 by A2, CARD_2:76 ;
then dom (Sgm {n,m}) = {1,2} by FINSEQ_1:4, FINSEQ_1:def 3;
then A5: ( 1 in dom (Sgm {n,m}) & 2 in dom (Sgm {n,m}) & rng (Sgm {n,m}) = {n,m} ) by A3, FINSEQ_1:def 13, TARSKI:def 2;
then A6: ( (Sgm {n,m}) . 1 in {n,m} & (Sgm {n,m}) . 2 in {n,m} ) by FUNCT_1:def 5;
A7: Sgm {n,m} is one-to-one by A3, Lm1;

now

per cases ( ( (Sgm {n,m}) . 1 = n & (Sgm {n,m}) . 2 = n ) or ( (Sgm {n,m}) . 1 = m & (Sgm {n,m}) . 2 = m ) or ( (Sgm {n,m}) . 1 = n & (Sgm {n,m}) . 2 = m ) or ( (Sgm {n,m}) . 1 = m & (Sgm {n,m}) . 2 = n ) ) by A6, TARSKI:def 2;

suppose ( (Sgm {n,m}) . 1 = n & (Sgm {n,m}) . 2 = n ) ; :: thesis: ( (Sgm {n,m}) . 1 = n & (Sgm {n,m}) . 2 = m )

hence ( (Sgm {n,m}) . 1 = n & (Sgm {n,m}) . 2 = m ) by A5, A7, FUNCT_1:def 8; :: thesis: verum

end;

suppose ( (Sgm {n,m}) . 1 = m & (Sgm {n,m}) . 2 = m ) ; :: thesis: ( (Sgm {n,m}) . 1 = n & (Sgm {n,m}) . 2 = m )

hence ( (Sgm {n,m}) . 1 = n & (Sgm {n,m}) . 2 = m ) by A5, A7, FUNCT_1:def 8; :: thesis: verum

end;

suppose ( (Sgm {n,m}) . 1 = n & (Sgm {n,m}) . 2 = m ) ; :: thesis: ( (Sgm {n,m}) . 1 = n & (Sgm {n,m}) . 2 = m )

hence ( (Sgm {n,m}) . 1 = n & (Sgm {n,m}) . 2 = m ) ; :: thesis: verum

end;

suppose ( (Sgm {n,m}) . 1 = m & (Sgm {n,m}) . 2 = n ) ; :: thesis: ( (Sgm {n,m}) . 1 = n & (Sgm {n,m}) . 2 = m )

hence ( (Sgm {n,m}) . 1 = n & (Sgm {n,m}) . 2 = m ) by A2, A3, A4, FINSEQ_1:def 13; :: thesis: verum

end;

end;

end;

hence Sgm {n,m} = <*n,m*> by A4, FINSEQ_1:61; :: thesis: verum