deffunc H1( 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 = H1(x)
from FUNCT_2:sch 4(); for b1, b2 being INT-Expression of X st ( for s being Element of Funcs (X,INT) holds b1 . s = s . (v . s) ) & ( for s being Element of Funcs (X,INT) holds b2 . s = s . (v . s) ) holds
b1 = b2
let f1, f2 be INT-Expression of X; ( ( 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)
; f1 = f2
hence
f1 = f2
; verum