let f1, f2 be Function of [:(bool (SetPrimes n)),(Seg n):],NAT; ( ( 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)
; f1 = f2
for x being object st x in [:(bool (SetPrimes n)),(Seg n):] holds
f1 . x = f2 . x
proof
let x be
object ;
( x in [:(bool (SetPrimes n)),(Seg n):] implies f1 . x = f2 . x )
assume G1:
x in [:(bool (SetPrimes n)),(Seg n):]
;
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
;
verum
end;
hence
f1 = f2
by FUNCT_2:12; verum