let f1, f2 be Function of [:(bool (SetPrimes n)),(Seg n):],NAT; :: 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
f1 . x = (Product ((A,1) -bag)) * (k ^2) ) & ( 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
f2 . x = (Product ((A,1) -bag)) * (k ^2) ) implies f1 = f2 )
assume that
A1: 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
f1 . x = (Product ((A,1) -bag)) * (k ^2) and
A2: 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
f2 . x = (Product ((A,1) -bag)) * (k ^2) ; :: thesis: f1 = f2
for x being object st x in [:(bool (SetPrimes n)),(Seg n):] holds
f1 . x = f2 . x

proof

let x be object ; :: thesis: ( x in [:(bool (SetPrimes n)),(Seg n):] implies f1 . x = f2 . x )
assume G1: x in [:(bool (SetPrimes n)),(Seg n):] ; :: thesis: f1 . x = f2 . x
then G0: x is pair by CARDFIL4:4;
then G3: x = [(x `1),(x `2)] ;
then reconsider xx = x `1 as Subset of (SetPrimes n) by G1, ZFMISC_1:87;
a4: SetPrimes n c= SetPrimes by XBOOLE_1:17;
xx c= SetPrimes by a4;
then reconsider xx = x `1 as finite Subset of SetPrimes ;
x `2 in Seg n by G1, G3, ZFMISC_1:87;
then reconsider yy = x `2 as Nat ;
G2: x = [xx,yy] by G0;
then f1 . x = (Product ((xx,1) -bag)) * (yy ^2) by G1, A1
.= f2 . x by A2, G1, G2 ;
hence f1 . x = f2 . x ; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:12; :: thesis: verum