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 A5, NAT_D:def 3;
consider d2 being Nat such that
A7: n = d * d2 by A4, NAT_D:def 3;
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 A6, A7, NAT_D:3;
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 A3, A6, ORDINAL1:def 12;
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 A9, ORDINAL1:def 12;
consider d2 being Nat such that
A12: n div p = d * d2 by A11, NAT_D:def 3;
(n div p) * p = (d * d2) * p by A12;
then n = d2 * (d * p) by A1, NAT_D:3;
then A13: d1 divides n by A9, NAT_D:def 3;
p divides d1 by A9, NAT_D:def 3;
hence x in { d where d is Element of NAT : ( d > 0 & d divides n & p divides d ) } by A9, A10, A13; :: thesis: verum