let n be natural number ; :: 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 A = { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } ;
set B = { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } ;
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 set ; :: 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 & d > 0 & d divides n & p divides d ) ;
consider d1 being Nat such that
A3: d = p * d1 by A2, NAT_D:def 3;
A4: d1 in NAT by ORDINAL1:def 13;
consider d2 being Nat such that
A5: n = d * d2 by A2, NAT_D:def 3;
n = p * (d1 * d2) by A3, A5;
then p divides n by NAT_D:def 3;
then p * (n div p) = p * (d1 * d2) by A3, A5, NAT_D:3;
then A6: n div p = d1 * d2 by XCMPLX_1:5;
d1 <> 0 by A2, A3;
then A7: d1 > 0 ;
d1 divides n div p by A6, NAT_D:def 3;
hence x in { (p * d) where d is Element of NAT : ( d > 0 & d divides n div p ) } by A2, A3, A4, A7; :: thesis: verum

end;

let x be set ; :: 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
A8: ( p * d = x & d > 0 & d divides n div p ) ;
reconsider d1 = x as Element of NAT by A8;
d1 <> 0 by A8;
then A9: d1 > 0 ;
consider d2 being Nat such that
A10: n div p = d * d2 by A8, NAT_D:def 3;
(n div p) * p = (d * d2) * p by A10;
then n = d2 * (d * p) by A1, NAT_D:3;
then A11: d1 divides n by A8, NAT_D:def 3;
p divides d1 by A8, NAT_D:def 3;
hence x in { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } by A9, A11; :: thesis: verum