let n be Ordinal; :: thesis: for i being Element of NAT
for b being bag of n st i in dom (divisors b) holds
(divisors b) /. i divides b
let i be Element of NAT ; :: thesis: for b being bag of n st i in dom (divisors b) holds
(divisors b) /. i divides b
let b be bag of n; :: thesis: ( i in dom (divisors b) implies (divisors b) /. i divides b )
assume i in dom (divisors b) ; :: thesis: (divisors b) /. i divides b
then A1: ( (divisors b) /. i = (divisors b) . i & (divisors b) . i in rng (divisors b) ) by FUNCT_1:def 3, PARTFUN1:def 6;
reconsider pid = (divisors b) /. i as bag of n ;
consider S being non empty finite Subset of (Bags n) such that
A2: divisors b = SgmX ((BagOrder n),S) and
A3: for p being bag of n holds
( p in S iff p divides b ) by Def15;
BagOrder n linearly_orders S by Lm4, ORDERS_1:38;
then pid in S by A2, A1, Def2;
hence (divisors b) /. i divides b by A3; :: thesis: verum