deffunc H₁( Element of Funcs X,INT ) -> Element of INT = $1 . x;
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 . x ) & ( for s being Element of Funcs X,INT holds b₂ . s = s . x ) holds
b₁ = b₂
let f1, f2 be INT-Expression of X; :: thesis: ( ( for s being Element of Funcs X,INT holds f1 . s = s . x ) & ( for s being Element of Funcs X,INT holds f2 . s = s . x ) implies f1 = f2 )
assume that
A1: for s being Element of Funcs X,INT holds f1 . s = s . x and
A2: for s being Element of Funcs X,INT holds f2 . s = s . x ; :: thesis: f1 = f2

now

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

end;

hence f1 = f2 by FUNCT_2:113; :: thesis: verum