let n be Nat; :: thesis: ( rng (prime_exponents (Product (primesFinS n))) c= {0,1} & card (support (prime_exponents (Product (primesFinS n)))) = n )
defpred S₁[ Nat] means ( card (support (prime_exponents (Product (primesFinS $1)))) = $1 & rng (prime_exponents (Product (primesFinS $1))) c= {0,1} );
A1: Product (primesFinS 0) = 1 by RVSUM_1:94;
then pfexp (Product (primesFinS 0)) = EmptyBag SetPrimes by NAT_3:39;
then pfexp (Product (primesFinS 0)) = SetPrimes --> {} by PBOOLE:def 3;
then A2: ( rng (pfexp (Product (primesFinS 0))) = {0} & {0} c= {0,1} ) by FUNCOP_1:8, ZFMISC_1:7;
support (pfexp (Product (primesFinS 0))) = {} by A1;
then card (support (pfexp (Product (primesFinS 0)))) = 0 ;
then A3: S₁[ 0 ] by A2;
A4: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
set pn = primenumber n;
set Pn = Product (primesFinS n);
set Pn1 = Product (primesFinS (n + 1));
assume A5: S₁[n] ; :: thesis: S₁[n + 1]
A6: Product (primesFinS (n + 1)) = (Product (primesFinS n)) * (primenumber n) by Th25;
A7: (support (pfexp (primenumber n))) \/ (support (pfexp (Product (primesFinS n)))) = support (pfexp (Product (primesFinS (n + 1)))) by A6, NAT_3:46;
n in NAT by ORDINAL1:def 12;
then primeindex (primenumber n) = n by NUMBER10:def 4;
then A8: primenumber n, Product (primesFinS n) are_coprime by Th30;
then support (pfexp (primenumber n)) misses support (pfexp (Product (primesFinS n))) by NAT_3:44;
then A9: card (support (pfexp (Product (primesFinS (n + 1))))) = (card (support (pfexp (primenumber n)))) + (card (support (pfexp (Product (primesFinS n))))) by A7, CARD_2:40;
card (support (pfexp (primenumber n))) = 1 by Th22;
hence card (support (pfexp (Product (primesFinS (n + 1))))) = n + 1 by A9, A5; :: thesis: rng (prime_exponents (Product (primesFinS (n + 1)))) c= {0,1}
A10: rng (pfexp ((Product (primesFinS n)) * (primenumber n))) = (rng (pfexp (Product (primesFinS n)))) \/ (rng (pfexp (primenumber n))) by A8, Th24;
A11: rng (pfexp (primenumber n)) c= {0,1} by Th22;
rng (pfexp (Product (primesFinS n))) c= {0,1} by A5;
then rng (pfexp (Product (primesFinS (n + 1)))) c= {0,1} by A6, A10, A11, XBOOLE_1:8;
hence rng (prime_exponents (Product (primesFinS (n + 1)))) c= {0,1} ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A4);
hence ( rng (prime_exponents (Product (primesFinS n))) c= {0,1} & card (support (prime_exponents (Product (primesFinS n)))) = n ) ; :: thesis: verum