deffunc H₁( set ) -> Element of NAT = IFEQ (t1 . $1),(t2 . $1),1,0 ;
consider f being Function such that
A25: ( dom f = (dom t1) /\ (dom t2) & ( for x being set st x in (dom t1) /\ (dom t2) holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
f is integer-yielding

proof

let x be set ; :: according to VALUED_0:def 11 :: thesis: ( not x in proj1 f or f . x is integer )
assume x in dom f ; :: thesis: f . x is integer
then f . x = H₁(x) by A25;
hence f . x is integer ; :: thesis: verum

end;

hence ex f being integer-yielding Function st
( dom f = (dom t1) /\ (dom t2) & ( for x being set st x in dom f holds
f . x = H₁(x) ) ) by A25; :: thesis: for b₁, b₂ being integer-yielding Function st dom b₁ = (dom t1) /\ (dom t2) & ( for s being set st s in dom b₁ holds
b₁ . s = IFEQ (t1 . s),(t2 . s),1,0 ) & dom b₂ = (dom t1) /\ (dom t2) & ( for s being set st s in dom b₂ holds
b₂ . s = IFEQ (t1 . s),(t2 . s),1,0 ) holds
b₁ = b₂
let f1, f2 be integer-yielding Function; :: thesis: ( dom f1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom f1 holds
f1 . s = IFEQ (t1 . s),(t2 . s),1,0 ) & dom f2 = (dom t1) /\ (dom t2) & ( for s being set st s in dom f2 holds
f2 . s = IFEQ (t1 . s),(t2 . s),1,0 ) implies f1 = f2 )
assume that
A26: dom f1 = (dom t1) /\ (dom t2) and
A27: for s being set st s in dom f1 holds
f1 . s = H₁(s) and
A28: dom f2 = (dom t1) /\ (dom t2) and
A29: for s being set st s in dom f2 holds
f2 . s = H₁(s) ; :: thesis: f1 = f2

now

let s be set ; :: thesis: ( s in (dom t1) /\ (dom t2) implies f1 . s = f2 . s )
assume A30: s in (dom t1) /\ (dom t2) ; :: thesis: f1 . s = f2 . s
hence f1 . s = H₁(s) by A26, A27
.= f2 . s by A28, A29, A30 ;
:: thesis: verum

end;

hence f1 = f2 by A26, A28, FUNCT_1:9; :: thesis: verum