let n be Ordinal; :: thesis: for i being Nat
for b, b1, b2 being bag of st i > 1 & i < len (divisors b) holds
( (divisors b) /. i <> EmptyBag n & (divisors b) /. i <> b )
let i be Nat; :: thesis: for b, b1, b2 being bag of st i > 1 & i < len (divisors b) holds
( (divisors b) /. i <> EmptyBag n & (divisors b) /. i <> b )
let b, b1, b2 be bag of ; :: thesis: ( i > 1 & i < len (divisors b) implies ( (divisors b) /. i <> EmptyBag n & (divisors b) /. i <> b ) )
A1: ( (divisors b) /. 1 = EmptyBag n & (divisors b) /. (len (divisors b)) = b ) by Th69;
A2: ( 1 in dom (divisors b) & len (divisors b) in dom (divisors b) ) by FINSEQ_5:6;
assume A3: ( i > 1 & i < len (divisors b) ) ; :: thesis: ( (divisors b) /. i <> EmptyBag n & (divisors b) /. i <> b )
then i in dom (divisors b) by FINSEQ_3:27;
hence ( (divisors b) /. i <> EmptyBag n & (divisors b) /. i <> b ) by A1, A2, A3, PARTFUN2:17; :: thesis: verum