defpred S₁[ object , object , object ] means for A being finite Subset of SetPrimes
for k being Nat st A = $1 & k = $2 holds
$3 = (Product ((A,1) -bag)) * (k ^2);
A1: for x, y, z1, z2 being object st x in bool (SetPrimes n) & y in Seg n & S₁[x,y,z1] & S₁[x,y,z2] holds
z1 = z2

proof

let x, y, z1, z2 be object ; :: thesis: ( x in bool (SetPrimes n) & y in Seg n & S₁[x,y,z1] & S₁[x,y,z2] implies z1 = z2 )
assume a1: ( x in bool (SetPrimes n) & y in Seg n & S₁[x,y,z1] & S₁[x,y,z2] ) ; :: thesis: z1 = z2
then reconsider xa = x as Subset of (SetPrimes n) ;
a4: SetPrimes n c= SetPrimes by XBOOLE_1:17;
xa c= SetPrimes by a4;
then reconsider S = xa as finite Subset of SetPrimes ;
set xx = (S,1) -bag ;
reconsider yy = y as Nat by a1;
z1 = (Product ((S,1) -bag)) * (yy ^2) by a1;
hence z1 = z2 by a1; :: thesis: verum

end;

A2: for x, y being object st x in bool (SetPrimes n) & y in Seg n holds
ex z being object st S₁[x,y,z]

proof

let x, y be object ; :: thesis: ( x in bool (SetPrimes n) & y in Seg n implies ex z being object st S₁[x,y,z] )
assume a1: ( x in bool (SetPrimes n) & y in Seg n ) ; :: thesis: ex z being object st S₁[x,y,z]
a4: SetPrimes n c= SetPrimes by XBOOLE_1:17;
reconsider xx = x as Subset of (SetPrimes n) by a1;
xx c= SetPrimes by a4;
then reconsider xx = x as finite Subset of SetPrimes ;
reconsider yy = y as Nat by a1;
ex z being object st S₁[x,y,z]

proof

take (Product ((xx,1) -bag)) * (yy ^2) ; :: thesis: S₁[x,y,(Product ((xx,1) -bag)) * (yy ^2)]
thus S₁[x,y,(Product ((xx,1) -bag)) * (yy ^2)] ; :: thesis: verum

end;

hence ex z being object st S₁[x,y,z] ; :: thesis: verum

end;

ex f being Function st
( dom f = [:(bool (SetPrimes n)),(Seg n):] & ( for x, y being object st x in bool (SetPrimes n) & y in Seg n holds
S₁[x,y,f . (x,y)] ) ) from FUNCT_3:sch 1(A1, A2);
then consider f being Function such that
D1: ( dom f = [:(bool (SetPrimes n)),(Seg n):] & ( for x, y being object st x in bool (SetPrimes n) & y in Seg n holds
S₁[x,y,f . (x,y)] ) ) ;
rng f c= NAT

proof

let g be object ; :: according to TARSKI:def 3 :: thesis: ( not g in rng f or g in NAT )
assume g in rng f ; :: thesis: g in NAT
then consider gg being object such that
E1: ( gg in dom f & g = f . gg ) by FUNCT_1:def 3;
G0: gg is pair by CARDFIL4:4, E1, D1;
then G3: gg = [(gg `1),(gg `2)] ;
then Z1: gg `1 in bool (SetPrimes n) by E1, D1, ZFMISC_1:87;
reconsider g1 = gg `1 as Subset of (SetPrimes n) by G3, E1, D1, ZFMISC_1:87;
a4: SetPrimes n c= SetPrimes by XBOOLE_1:17;
g1 c= SetPrimes by a4;
then reconsider g1 = gg `1 as finite Subset of SetPrimes ;
Z2: gg `2 in Seg n by E1, D1, G3, ZFMISC_1:87;
then reconsider yy = gg `2 as Nat ;
f . (g1,yy) = (Product ((g1,1) -bag)) * (yy ^2) by Z1, D1, Z2;
hence g in NAT by E1, G0; :: thesis: verum

end;

then reconsider f = f as Function of [:(bool (SetPrimes n)),(Seg n):],NAT by D1, FUNCT_2:2;
take f ; :: thesis: for x being Element of [:(bool (SetPrimes n)),(Seg n):]
for A being finite Subset of SetPrimes
for k being Nat st x = [A,k] holds
f . x = (Product ((A,1) -bag)) * (k ^2)
let x be Element of [:(bool (SetPrimes n)),(Seg n):]; :: thesis: for A being finite Subset of SetPrimes
for k being Nat st x = [A,k] holds
f . x = (Product ((A,1) -bag)) * (k ^2)
let A be finite Subset of SetPrimes; :: thesis: for k being Nat st x = [A,k] holds
f . x = (Product ((A,1) -bag)) * (k ^2)
let k be Nat; :: thesis: ( x = [A,k] implies f . x = (Product ((A,1) -bag)) * (k ^2) )
assume D2: x = [A,k] ; :: thesis: f . x = (Product ((A,1) -bag)) * (k ^2)
then D3: A in bool (SetPrimes n) by ZFMISC_1:87;
k in Seg n by D2, ZFMISC_1:87;
then S₁[A,k,f . (A,k)] by D3, D1;
hence f . x = (Product ((A,1) -bag)) * (k ^2) by D2; :: thesis: verum