deffunc H1( object ) -> Element of NAT = IFEQ ((t1 . $1),(t2 . $1),1,0);
consider f being Function such that
A33: ( dom f = (dom t1) /\ (dom t2) & ( for x being object st x in (dom t1) /\ (dom t2) holds
f . x = H1(x) ) ) from FUNCT_1:sch 3();
 f is INT -valued
proof
let y be object ; :: according to TARSKI:def 3,RELAT_1:def 19 :: thesis: ( not y in proj2 f or y in INT )
assume y in rng f ; :: thesis: y in INT
then consider x being object such that
A34: x in dom f and
A35: f . x = y by FUNCT_1:def 3;
f . x = H1(x) by A33, A34;
hence y in INT by A35, INT_1:def 2; :: thesis: verum
end;
hence ex f being INT -valued Function st
( dom f = (dom t1) /\ (dom t2) & ( for x being object st x in dom f holds
f . x = H1(x) ) ) by A33; :: thesis: for b1, b2 being INT -valued Function st dom b1 = (dom t1) /\ (dom t2) & ( for s being object st s in dom b1 holds
b1 . s = IFEQ ((t1 . s),(t2 . s),1,0) ) & dom b2 = (dom t1) /\ (dom t2) & ( for s being object st s in dom b2 holds
b2 . s = IFEQ ((t1 . s),(t2 . s),1,0) ) holds
b1 = b2
let f1, f2 be INT -valued Function; :: thesis: ( dom f1 = (dom t1) /\ (dom t2) & ( for s being object st s in dom f1 holds
f1 . s = IFEQ ((t1 . s),(t2 . s),1,0) ) & dom f2 = (dom t1) /\ (dom t2) & ( for s being object st s in dom f2 holds
f2 . s = IFEQ ((t1 . s),(t2 . s),1,0) ) implies f1 = f2 )
assume that
A36: dom f1 = (dom t1) /\ (dom t2) and
A37: for s being object st s in dom f1 holds
f1 . s = H1(s) and
A38: dom f2 = (dom t1) /\ (dom t2) and
A39: for s being object st s in dom f2 holds
f2 . s = H1(s) ; :: thesis: f1 = f2
now :: thesis: for s being object st s in (dom t1) /\ (dom t2) holds
f1 . s = f2 . s
let s be object ; :: thesis: ( s in (dom t1) /\ (dom t2) implies f1 . s = f2 . s )
assume A40: s in (dom t1) /\ (dom t2) ; :: thesis: f1 . s = f2 . s
hence f1 . s = H1(s) by A36, A37
.= f2 . s by A38, A39, A40 ;
:: thesis: verum
end;
hence f1 = f2 by A36, A38; :: thesis: verum