let F, G be FinSequence of 2 -tuples_on (Bags n); :: thesis: ( dom F = dom (divisors b) & ( for i being Element of NAT
for p being bag of n st i in dom F & p = (divisors b) /. i holds
F /. i = <*p,(b -' p)*> ) & dom G = dom (divisors b) & ( for i being Element of NAT
for p being bag of n st i in dom G & p = (divisors b) /. i holds
G /. i = <*p,(b -' p)*> ) implies F = G )
assume that
A6: dom F = dom (divisors b) and
A7: for i being Element of NAT
for p being bag of n st i in dom F & p = (divisors b) /. i holds
F /. i = <*p,(b -' p)*> and
A8: dom G = dom (divisors b) and
A9: for i being Element of NAT
for p being bag of n st i in dom G & p = (divisors b) /. i holds
G /. i = <*p,(b -' p)*> ; :: thesis: F = G

now

let i be Nat; :: thesis: ( i in dom F implies F /. i = G /. i )
reconsider p = (divisors b) /. i as bag of n ;
assume A10: i in dom F ; :: thesis: F /. i = G /. i
hence F /. i = <*p,(b -' p)*> by A7
.= G /. i by A6, A8, A9, A10 ;
:: thesis: verum

end;

hence F = G by A6, A8, FINSEQ_5:13; :: thesis: verum