deffunc H₁( Element of Funcs (X,INT)) -> Element of INT = $1 . (v . $1);
thus ex f being Function of (Funcs (X,INT)),INT st
for x being Element of Funcs (X,INT) holds f . x = H₁(x) from FUNCT_2:sch 4(); :: thesis: for b₁, b₂ being INT-Expression of X st ( for s being Element of Funcs (X,INT) holds b₁ . s = s . (v . s) ) & ( for s being Element of Funcs (X,INT) holds b₂ . s = s . (v . s) ) holds
b₁ = b₂
let f1, f2 be INT-Expression of X; :: thesis: ( ( for s being Element of Funcs (X,INT) holds f1 . s = s . (v . s) ) & ( for s being Element of Funcs (X,INT) holds f2 . s = s . (v . s) ) implies f1 = f2 )
assume that
A1: for s being Element of Funcs (X,INT) holds f1 . s = s . (v . s) and
A2: for s being Element of Funcs (X,INT) holds f2 . s = s . (v . s) ; :: thesis: f1 = f2

now :: thesis: for s being Element of Funcs (X,INT) holds f1 . s = f2 . s

let s be Element of Funcs (X,INT); :: thesis: f1 . s = f2 . s
thus f1 . s = s . (v . s) by A1
.= f2 . s by A2 ; :: thesis: verum

end;

hence f1 = f2 ; :: thesis: verum