let n be Nat; :: thesis: for p being Prime st p divides n holds
{ d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } = { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) }

let p be Prime; :: thesis: ( p divides n implies { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } = { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } )
assume A1: p divides n ; :: thesis: { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } = { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) }
set B = { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } ;
set A = { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } ;
thus { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } c= { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } :: according to XBOOLE_0:def 10 :: thesis: { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } c= { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } or x in { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } )
assume x in { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } ; :: thesis: x in { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) }
then consider d being Element of NAT such that
A2: d = x and
A3: d > 0 and
A4: d divides n and
A5: p divides d ;
consider d1 being Nat such that
A6: d = p * d1 by ;
consider d2 being Nat such that
A7: n = d * d2 by ;
n = p * (d1 * d2) by A6, A7;
then p divides n by NAT_D:def 3;
then p * (n div p) = p * (d1 * d2) by ;
then n div p = d1 * d2 by XCMPLX_1:5;
then A8: d1 divides n div p by NAT_D:def 3;
( d1 in NAT & d1 > 0 ) by ;
hence x in { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } by A2, A6, A8; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } or x in { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } )
assume x in { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } ; :: thesis: x in { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) }
then consider d being Element of NAT such that
A9: p * d = x and
A10: d > 0 and
A11: d divides n div p ;
reconsider d1 = x as Element of NAT by ;
consider d2 being Nat such that
A12: n div p = d * d2 by ;
(n div p) * p = (d * d2) * p by A12;
then n = d2 * (d * p) by ;
then A13: d1 divides n by ;
p divides d1 by ;
hence x in { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } by A9, A10, A13; :: thesis: verum