let m, n be Nat; :: 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:3;
A4: n in Seg n by A1, FINSEQ_1:3;
Seg n c= Seg m by A2, FINSEQ_1:5;
then A5: {n,m} c= Seg m by A3, A4, ZFMISC_1:32;
then A6: Sgm {n,m} is one-to-one by Lm1;
A7: len (Sgm {n,m}) = card {n,m} by A5, Th37
.= 2 by A2, CARD_2:57 ;
then A8: dom (Sgm {n,m}) = {1,2} by FINSEQ_1:2, 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 3;
A13: (Sgm {n,m}) . 1 in {n,m} by A9, A11, FUNCT_1:def 3;
now :: thesis: ( (Sgm {n,m}) . 1 = n & (Sgm {n,m}) . 2 = m )
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; :: 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; :: 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:44; :: thesis: verum