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 :: 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 . x by A1
.= f2 . s by A2 ; :: thesis: verum

end;

hence f1 = f2 ; :: thesis: verum