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
A6: ( dom F1 = REAL * & ( for f being Element of REAL * holds F1 . f = Relax f,n ) ) and
A7: ( dom F2 = REAL * & ( for f being Element of REAL * holds F2 . f = Relax f,n ) ) ; :: thesis: F1 = F2

now

let xx be set ; :: 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 A6;
thus F1 . xx = Relax h,n by A6
.= F2 . xx by A7 ; :: thesis: verum

end;

hence F1 = F2 by A6, A7, FUNCT_1:9; :: thesis: verum