let n be Ordinal; :: thesis: for b, b1 being bag of n holds
( b1 in rng (divisors b) iff b1 divides b )
let b, b1 be bag of n; :: thesis: ( b1 in rng (divisors b) iff b1 divides b )
consider S being non empty finite Subset of (Bags n) such that
A1: divisors b = SgmX ((BagOrder n),S) and
A2: for p being bag of n holds
( p in S iff p divides b ) by PRE_POLY:def 16;
field (BagOrder n) = Bags n by ORDERS_1:15;
then A3: BagOrder n linearly_orders S by ORDERS_1:37, ORDERS_1:38;
hereby :: thesis: ( b1 divides b implies b1 in rng (divisors b) )
assume b1 in rng (divisors b) ; :: thesis: b1 divides b
then b1 in S by A1, A3, PRE_POLY:def 2;
hence b1 divides b by A2; :: thesis: verum
end;
assume b1 divides b ; :: thesis: b1 in rng (divisors b)
then b1 in S by A2;
hence b1 in rng (divisors b) by A1, A3, PRE_POLY:def 2; :: thesis: verum