n >= 1 by NAT_1:14;

per cases then ( n = 1 or n > 1 ) by XXREAL_0:1;

suppose A1: n = 1 ; :: thesis: ex b₁ being Function st
( dom b₁ = support (ppf n) & ( for p being Nat st p in dom b₁ holds
b₁ . p = p - 1 ) )

take {} ; :: thesis: ( dom {} = support (ppf n) & ( for p being Nat st p in dom {} holds
{} . p = p - 1 ) )
support (ppf 1) = support (pfexp 1) by NAT_3:def 9;
hence ( dom {} = support (ppf n) & ( for p being Nat st p in dom {} holds
{} . p = p - 1 ) ) by A1; :: thesis: verum

end;

suppose n > 1 ; :: thesis: ex b₁ being Function st
( dom b₁ = support (ppf n) & ( for p being Nat st p in dom b₁ holds
b₁ . p = p - 1 ) )

then reconsider A = support (ppf n) as non empty natural-membered set by NAT_3:57;
consider f being Function such that
A2: ( dom f = A & ( for d being Element of A holds f . d = H₁(d) ) ) from FUNCT_1:sch 4();
take f ; :: thesis: ( dom f = support (ppf n) & ( for p being Nat st p in dom f holds
f . p = p - 1 ) )
thus ( dom f = support (ppf n) & ( for p being Nat st p in dom f holds
f . p = p - 1 ) ) by A2; :: thesis: verum

end;

end;