let f1, f2 be ManySortedSet of SetPrimes ; :: thesis: ( support f1 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
f1 . p = p |^ (2 * ((p |-count n) div 2)) ) & support f2 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
f2 . p = p |^ (2 * ((p |-count n) div 2)) ) implies f1 = f2 )
assume that
A16: support f1 = support (pfexp n) and
A17: for p being Nat st p in support (pfexp n) holds
f1 . p = p |^ (2 * ((p |-count n) div 2)) and
A18: support f2 = support (pfexp n) and
A19: for p being Nat st p in support (pfexp n) holds
f2 . p = p |^ (2 * ((p |-count n) div 2)) ; :: thesis: f1 = f2
now :: thesis: for i being object st i in SetPrimes holds
f1 . i = f2 . i
let i be object ; :: thesis: ( i in SetPrimes implies f1 . b1 = f2 . b1 )
assume A20: i in SetPrimes ; :: thesis: f1 . b1 = f2 . b1
reconsider p = i as prime Nat by A20, NEWTON:def 6;
per cases ( p in support (pfexp n) or not p in support (pfexp n) ) ;
suppose A21: p in support (pfexp n) ; :: thesis: f1 . b1 = f2 . b1
hence f1 . i = p |^ (2 * ((p |-count n) div 2)) by A17
.= f2 . i by A19, A21 ;
:: thesis: verum
end;
suppose A22: not p in support (pfexp n) ; :: thesis: f1 . b1 = f2 . b1
hence f1 . i = 0 by A16, PRE_POLY:def 7
.= f2 . i by A18, A22, PRE_POLY:def 7 ;
:: thesis: verum
end;
end;
end;
hence f1 = f2 by PBOOLE:3; :: thesis: verum