let b be bag of 1; :: thesis: ( SgmX ((BagOrder 1),(rng (divisors b))) = XFS2FS (NBag1 | (Segm ((b . 0) + 1))) & divisors b = XFS2FS (NBag1 | (Segm ((b . 0) + 1))) )
set F = NBag1 | (Segm ((b . 0) + 1));
A1: rng (XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) = rng (NBag1 | (Segm ((b . 0) + 1))) by AFINSQ_1:97
.= { x where x is bag of 1 : x . 0 <= b . 0 } by Th14
.= rng (divisors b) by Th13 ;
A2: len (NBag1 | (Segm ((b . 0) + 1))) = (b . 0) + 1 ;
A3: for n, m being Nat st n in dom (XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) & m in dom (XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) & n < m holds
( (XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. n <> (XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. m & [((XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. n),((XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. m)] in BagOrder 1 )

proof

let n, m be Nat; :: thesis: ( n in dom (XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) & m in dom (XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) & n < m implies ( (XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. n <> (XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. m & [((XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. n),((XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. m)] in BagOrder 1 ) )
assume A4: ( n in dom (XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) & m in dom (XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) & n < m ) ; :: thesis: ( (XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. n <> (XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. m & [((XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. n),((XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. m)] in BagOrder 1 )
A5: (XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. n <> (XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. m

proof

assume (XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. n = (XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. m ; :: thesis: contradiction
then (XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) . n = (XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. m by A4, PARTFUN1:def 6
.= (XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) . m by A4, PARTFUN1:def 6 ;
hence contradiction by A4, FUNCT_1:def 4; :: thesis: verum

end;

len (XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) = len (NBag1 | (Segm ((b . 0) + 1))) by AFINSQ_1:def 9;
then A6: ( n in Seg (len (NBag1 | (Segm ((b . 0) + 1)))) & m in Seg (len (NBag1 | (Segm ((b . 0) + 1)))) ) by A4, FINSEQ_1:def 3;
then A7: ( 1 <= n & n <= (b . 0) + 1 & 1 <= m & m <= (b . 0) + 1 ) by FINSEQ_1:1;
then A8: n - 1 = n -' 1 by XREAL_1:233;
A9: ( n < m & m <= (b . 0) + 1 ) by A6, FINSEQ_1:1, A4;
then A10: n < (b . 0) + 1 by XXREAL_0:2;
A11: ( 1 <= n & n < (b . 0) + 1 ) by A6, FINSEQ_1:1, A9, XXREAL_0:2;
A12: m - 1 = m -' 1 by A7, XREAL_1:233;
n - 1 <= n by A8, NAT_D:35;
then n - 1 < (b . 0) + 1 by A10, XXREAL_0:2;
then A13: n - 1 in dom (NBag1 | (Segm ((b . 0) + 1))) by A8, NAT_1:44;
A14: (XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. n = (XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) . n by A4, PARTFUN1:def 6
.= (NBag1 | (Segm ((b . 0) + 1))) . (n - 1) by A2, A11, AFINSQ_1:def 9
.= NBag1 . (n - 1) by A13, FUNCT_1:47
.= 1 --> (n - 1) by A8, Def1 ;
A15: 0 in 1 by CARD_1:49, TARSKI:def 1;
then A16: (1 --> (n -' 1)) . 0 = n -' 1 by FUNCOP_1:7;
A17: (1 --> (m -' 1)) . 0 = m -' 1 by A15, FUNCOP_1:7;
[((XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. n),((XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. m)] in BagOrder 1

proof

A18: m -' 1 in dom (NBag1 | (Segm ((b . 0) + 1)))

proof

per cases ( m = (b . 0) + 1 or m <> (b . 0) + 1 ) ;

suppose A19: m = (b . 0) + 1 ; :: thesis: m -' 1 in dom (NBag1 | (Segm ((b . 0) + 1)))

(b . 0) + 0 < (b . 0) + 1 by XREAL_1:8;
hence m -' 1 in dom (NBag1 | (Segm ((b . 0) + 1))) by A19, NAT_1:44; :: thesis: verum

end;

suppose m <> (b . 0) + 1 ; :: thesis: m -' 1 in dom (NBag1 | (Segm ((b . 0) + 1)))

then A20: ( 1 <= m & m < (b . 0) + 1 ) by A7, XXREAL_0:1;
m -' 1 <= m by NAT_D:35;
then m -' 1 < (b . 0) + 1 by A20, XXREAL_0:2;
hence m -' 1 in dom (NBag1 | (Segm ((b . 0) + 1))) by NAT_1:44; :: thesis: verum

end;

end;

end;

A21: (XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. m = (XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) . m by A4, PARTFUN1:def 6
.= (NBag1 | (Segm ((b . 0) + 1))) . (m - 1) by A2, A7, AFINSQ_1:def 9
.= NBag1 . (m - 1) by A12, A18, FUNCT_1:47
.= 1 --> (m - 1) by A12, Def1 ;
1 --> (n -' 1) divides 1 --> (m -' 1) by A16, A8, A12, A4, XREAL_1:9, A17, Th8;
then 1 --> (n -' 1) <=' 1 --> (m -' 1) by PRE_POLY:49;
hence [((XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. n),((XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. m)] in BagOrder 1 by A8, A12, A21, A14, PRE_POLY:def 14; :: thesis: verum

end;

hence ( (XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. n <> (XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. m & [((XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. n),((XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. m)] in BagOrder 1 ) by A5; :: thesis: verum

end;

reconsider S = rng (divisors b) as non empty finite Subset of (Bags 1) ;
A22: SgmX ((BagOrder 1),S) = XFS2FS (NBag1 | (Segm ((b . 0) + 1))) by A3, PRE_POLY:9, A1;
for p being bag of 1 holds
( p in S iff p divides b ) by Th12;
hence ( SgmX ((BagOrder 1),(rng (divisors b))) = XFS2FS (NBag1 | (Segm ((b . 0) + 1))) & divisors b = XFS2FS (NBag1 | (Segm ((b . 0) + 1))) ) by A22, PRE_POLY:def 16; :: thesis: verum