let f, g be Function; :: thesis: ( dom f = support (ppf n) & ( for p being Nat st p in dom f holds
ex c being non zero Nat st
( c = p |-count n & f . p = p |^ (c - 1) ) ) & dom g = support (ppf n) & ( for p being Nat st p in dom g holds
ex c being non zero Nat st
( c = p |-count n & g . p = p |^ (c - 1) ) ) implies f = g )
assume that
A12: dom f = support (ppf n) and
A13: for p being Nat st p in dom f holds
ex c being non zero Nat st
( c = p |-count n & f . p = p |^ (c - 1) ) and
A14: dom g = support (ppf n) and
A15: for p being Nat st p in dom g holds
ex c being non zero Nat st
( c = p |-count n & g . p = p |^ (c - 1) ) ; :: thesis: f = g
thus dom f = dom g by A12, A14; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in proj1 f or f . b₁ = g . b₁ )
let p be object ; :: thesis: ( not p in proj1 f or f . p = g . p )
assume A16: p in dom f ; :: thesis: f . p = g . p
reconsider p = p as Nat by A12, A16;
A17: ex c being non zero Nat st
( c = p |-count n & f . p = p |^ (c - 1) ) by A13, A16;
ex c being non zero Nat st
( c = p |-count n & g . p = p |^ (c - 1) ) by A12, A14, A15, A16;
hence f . p = g . p by A17; :: thesis: verum