deffunc H_{1}( object ) -> object = IFGT ((t1 . $1),(t2 . $1),0,1);

consider f being Function such that

A17: ( dom f = (dom t1) /\ (dom t2) & ( for x being object st x in (dom t1) /\ (dom t2) holds

f . x = H_{1}(x) ) )
from FUNCT_1:sch 3();

f is INT -valued

( dom f = (dom t1) /\ (dom t2) & ( for x being object st x in dom f holds

f . x = H_{1}(x) ) )
by A17; :: thesis: for b_{1}, b_{2} being INT -valued Function st dom b_{1} = (dom t1) /\ (dom t2) & ( for s being object st s in dom b_{1} holds

b_{1} . s = IFGT ((t1 . s),(t2 . s),0,1) ) & dom b_{2} = (dom t1) /\ (dom t2) & ( for s being object st s in dom b_{2} holds

b_{2} . s = IFGT ((t1 . s),(t2 . s),0,1) ) holds

b_{1} = b_{2}

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 = IFGT ((t1 . s),(t2 . s),0,1) ) & dom f2 = (dom t1) /\ (dom t2) & ( for s being object st s in dom f2 holds

f2 . s = IFGT ((t1 . s),(t2 . s),0,1) ) implies f1 = f2 )

assume that

A20: dom f1 = (dom t1) /\ (dom t2) and

A21: for s being object st s in dom f1 holds

f1 . s = H_{1}(s)
and

A22: dom f2 = (dom t1) /\ (dom t2) and

A23: for s being object st s in dom f2 holds

f2 . s = H_{1}(s)
; :: thesis: f1 = f2

consider f being Function such that

A17: ( dom f = (dom t1) /\ (dom t2) & ( for x being object st x in (dom t1) /\ (dom t2) holds

f . x = H

f is INT -valued

proof

hence
ex f being INT -valued Function st
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

A18: x in dom f and

A19: f . x = y by FUNCT_1:def 3;

f . x = H_{1}(x)
by A17, A18;

hence y in INT by A19, INT_1:def 2; :: thesis: verum

end;assume y in rng f ; :: thesis: y in INT

then consider x being object such that

A18: x in dom f and

A19: f . x = y by FUNCT_1:def 3;

f . x = H

hence y in INT by A19, INT_1:def 2; :: thesis: verum

( dom f = (dom t1) /\ (dom t2) & ( for x being object st x in dom f holds

f . x = H

b

b

b

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 = IFGT ((t1 . s),(t2 . s),0,1) ) & dom f2 = (dom t1) /\ (dom t2) & ( for s being object st s in dom f2 holds

f2 . s = IFGT ((t1 . s),(t2 . s),0,1) ) implies f1 = f2 )

assume that

A20: dom f1 = (dom t1) /\ (dom t2) and

A21: for s being object st s in dom f1 holds

f1 . s = H

A22: dom f2 = (dom t1) /\ (dom t2) and

A23: for s being object st s in dom f2 holds

f2 . s = H

now :: thesis: for s being object st s in (dom t1) /\ (dom t2) holds

f1 . s = f2 . s

hence
f1 = f2
by A20, A22; :: thesis: verumf1 . s = f2 . s

let s be object ; :: thesis: ( s in (dom t1) /\ (dom t2) implies f1 . s = f2 . s )

assume A24: s in (dom t1) /\ (dom t2) ; :: thesis: f1 . s = f2 . s

hence f1 . s = H_{1}(s)
by A20, A21

.= f2 . s by A22, A23, A24 ;

:: thesis: verum

end;assume A24: s in (dom t1) /\ (dom t2) ; :: thesis: f1 . s = f2 . s

hence f1 . s = H

.= f2 . s by A22, A23, A24 ;

:: thesis: verum