set X = REAL * ;

let F1, F2 be Element of Funcs ((REAL *),(REAL *)); :: thesis: ( dom F1 = REAL * & ( for f being Element of REAL * holds F1 . f = Relax (f,n) ) & dom F2 = REAL * & ( for f being Element of REAL * holds F2 . f = Relax (f,n) ) implies F1 = F2 )

assume that

A5: dom F1 = REAL * and

A6: for f being Element of REAL * holds F1 . f = Relax (f,n) and

A7: dom F2 = REAL * and

A8: for f being Element of REAL * holds F2 . f = Relax (f,n) ; :: thesis: F1 = F2

let F1, F2 be Element of Funcs ((REAL *),(REAL *)); :: thesis: ( dom F1 = REAL * & ( for f being Element of REAL * holds F1 . f = Relax (f,n) ) & dom F2 = REAL * & ( for f being Element of REAL * holds F2 . f = Relax (f,n) ) implies F1 = F2 )

assume that

A5: dom F1 = REAL * and

A6: for f being Element of REAL * holds F1 . f = Relax (f,n) and

A7: dom F2 = REAL * and

A8: for f being Element of REAL * holds F2 . f = Relax (f,n) ; :: thesis: F1 = F2

now :: thesis: for xx being object st xx in dom F1 holds

F1 . xx = F2 . xx

hence
F1 = F2
by A5, A7, FUNCT_1:2; :: thesis: verumF1 . xx = F2 . xx

let xx be object ; :: thesis: ( xx in dom F1 implies F1 . xx = F2 . xx )

assume xx in dom F1 ; :: thesis: F1 . xx = F2 . xx

then reconsider h = xx as Element of REAL * by A5;

thus F1 . xx = Relax (h,n) by A6

.= F2 . xx by A8 ; :: thesis: verum

end;assume xx in dom F1 ; :: thesis: F1 . xx = F2 . xx

then reconsider h = xx as Element of REAL * by A5;

thus F1 . xx = Relax (h,n) by A6

.= F2 . xx by A8 ; :: thesis: verum