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