deffunc H_{1}( 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_{1}(x)
from FUNCT_2:sch 4(); :: thesis: for b_{1}, b_{2} being INT-Expression of X st ( for s being Element of Funcs (X,INT) holds b_{1} . s = s . x ) & ( for s being Element of Funcs (X,INT) holds b_{2} . s = s . x ) holds

b_{1} = b_{2}

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

thus ex f being Function of (Funcs (X,INT)),INT st

for x being Element of Funcs (X,INT) holds f . x = H

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

hence
f1 = f2
; :: thesis: verumlet 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;thus f1 . s = s . x by A1

.= f2 . s by A2 ; :: thesis: verum