let n be Ordinal; :: thesis: for i being Nat
for b, b1, b2 being bag of n 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 n st i > 1 & i < len (divisors b) holds
( (divisors b) /. i <> EmptyBag n & (divisors b) /. i <> b )
let b, b1, b2 be bag of n; :: thesis: ( i > 1 & i < len (divisors b) implies ( (divisors b) /. i <> EmptyBag n & (divisors b) /. i <> b ) )
A1: ( 1 in dom (divisors b) & len (divisors b) in dom (divisors b) ) by FINSEQ_5:6;
A2: ( (divisors b) /. 1 = EmptyBag n & (divisors b) /. (len (divisors b)) = b ) by Th63;
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:25;
hence ( (divisors b) /. i <> EmptyBag n & (divisors b) /. i <> b ) by A2, A1, A3, PARTFUN2:10; :: thesis: verum