defpred S1[ Nat, set ] means for p being bag of n st p = (divisors b) /. $1 holds
$2 = <*p,(b -' p)*>;
A1: for k being Nat st k in Seg (len (divisors b)) holds
ex d being Element of 2 -tuples_on (Bags n) st S1[k,d]
proof
let k be Nat; :: thesis: ( k in Seg (len (divisors b)) implies ex d being Element of 2 -tuples_on (Bags n) st S1[k,d] )
assume k in Seg (len (divisors b)) ; :: thesis: ex d being Element of 2 -tuples_on (Bags n) st S1[k,d]
reconsider p = (divisors b) /. k as bag of n ;
reconsider b1 = p, b2 = b -' p as Element of Bags n by Def12;
len <*p,(b -' p)*> = 2 by FINSEQ_1:44;
then reconsider d = <*b1,b2*> as Element of 2 -tuples_on (Bags n) by FINSEQ_2:92;
take d ; :: thesis: S1[k,d]
thus S1[k,d] ; :: thesis: verum
end;
consider f being FinSequence of 2 -tuples_on (Bags n) such that
A2: len f = len (divisors b) and
A3: for n being Nat st n in Seg (len (divisors b)) holds
S1[n,f /. n] from FINSEQ_4:sch 1(A1);
 take f ; :: 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)*> ) )
thus dom f = dom (divisors b) by A2, FINSEQ_3:29; :: thesis: 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)*>
let i be Element of NAT ; :: thesis: for p being bag of n st i in dom f & p = (divisors b) /. i holds
f /. i = <*p,(b -' p)*>
let p be bag of n; :: thesis: ( i in dom f & p = (divisors b) /. i implies f /. i = <*p,(b -' p)*> )
assume that
A4: i in dom f and
A5: p = (divisors b) /. i ; :: thesis: f /. i = <*p,(b -' p)*>
i in Seg (len (divisors b)) by A2, A4, FINSEQ_1:def 3;
hence f /. i = <*p,(b -' p)*> by A3, A5; :: thesis: verum