let f, g be Function; :: thesis: ( dom f = support (ppf n) & ( for p being Nat st p in dom f holds
f . p = p - 1 ) & dom g = support (ppf n) & ( for p being Nat st p in dom g holds
g . p = p - 1 ) implies f = g )
assume that
A3: dom f = support (ppf n) and
A4: for p being Nat st p in dom f holds
f . p = H₁(p) and
A5: dom g = support (ppf n) and
A6: for p being Nat st p in dom g holds
g . p = H₁(p) ; :: thesis: f = g
thus dom f = dom g by A3, A5; :: 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 A7: p in dom f ; :: thesis: f . p = g . p
reconsider p = p as Nat by A3, A7;
f . p = H₁(p) by A4, A7
.= g . p by A3, A5, A6, A7 ;
hence f . p = g . p ; :: thesis: verum