let b be bag of 1; :: thesis: rng (divisors b) = { x where x is bag of 1 : x . 0 <= b . 0 }
A1: for o being object st o in { x where x is bag of 1 : x . 0 <= b . 0 } holds
o in rng (divisors b)

proof

let o be object ; :: thesis: ( o in { x where x is bag of 1 : x . 0 <= b . 0 } implies o in rng (divisors b) )
assume o in { x where x is bag of 1 : x . 0 <= b . 0 } ; :: thesis: o in rng (divisors b)
then consider x1 being bag of 1 such that
A2: ( o = x1 & x1 . 0 <= b . 0 ) ;
thus o in rng (divisors b) by A2, Th12; :: thesis: verum

end;

for o being object st o in rng (divisors b) holds
o in { x where x is bag of 1 : x . 0 <= b . 0 }

proof

let o be object ; :: thesis: ( o in rng (divisors b) implies o in { x where x is bag of 1 : x . 0 <= b . 0 } )
assume A3: o in rng (divisors b) ; :: thesis: o in { x where x is bag of 1 : x . 0 <= b . 0 }
then reconsider x1 = o as bag of 1 ;
x1 . 0 <= b . 0 by A3, Th12;
hence o in { x where x is bag of 1 : x . 0 <= b . 0 } ; :: thesis: verum

end;

hence rng (divisors b) = { x where x is bag of 1 : x . 0 <= b . 0 } by A1, TARSKI:2; :: thesis: verum