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*>
A3: m in Seg m by A2, FINSEQ_1:5;
A4: n in Seg n by A1, FINSEQ_1:5;
Seg n c= Seg m by A2, FINSEQ_1:7;
then A5: {n,m} c= Seg m by A3, A4, ZFMISC_1:38;
then A6: Sgm {n,m} is one-to-one by Lm1;
A7: len (Sgm {n,m}) = card {n,m} by A5, Th44
.= 2 by A2, CARD_2:76 ;
then A8: dom (Sgm {n,m}) = {1,2} by FINSEQ_1:4, FINSEQ_1:def 3;
then A9: 1 in dom (Sgm {n,m}) by TARSKI:def 2;
A10: 2 in dom (Sgm {n,m}) by A8, TARSKI:def 2;
A11: rng (Sgm {n,m}) = {n,m} by A5, FINSEQ_1:def 13;
then A12: (Sgm {n,m}) . 2 in {n,m} by A10, FUNCT_1:def 5;
A13: (Sgm {n,m}) . 1 in {n,m} by A9, A11, FUNCT_1:def 5;

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 A13, A12, 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 A9, A10, A6, 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 A9, A10, A6, 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, A5, A7, FINSEQ_1:def 13; :: thesis: verum

end;

end;

end;

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