let n be Ordinal; :: thesis: for i being Element of NAT
for b being bag of st i in dom (divisors b) holds
(divisors b) /. i divides b
let i be Element of NAT ; :: thesis: for b being bag of st i in dom (divisors b) holds
(divisors b) /. i divides b
let b be bag of ; :: thesis: ( i in dom (divisors b) implies (divisors b) /. i divides b )
assume A1: i in dom (divisors b) ; :: thesis: (divisors b) /. i divides b
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 holds
( p in S iff p divides b ) by Def18;
A4: BagOrder n linearly_orders S by Lm4, ORDERS_1:134;
A5: (divisors b) /. i = (divisors b) . i by A1, PARTFUN1:def 8;
(divisors b) /. i is Element of Bags n ;
then reconsider pid = (divisors b) /. i as bag of ;
(divisors b) . i in rng (divisors b) by A1, FUNCT_1:def 5;
then pid in S by A2, A4, A5, TRIANG_1:def 2;
hence (divisors b) /. i divides b by A3; :: thesis: verum