let F be non empty functional set ; :: thesis: for x, y being set

for g being Element of F holds

( g in F \ (x,y) iff g . x <> y )

let x, y be set ; :: thesis: for g being Element of F holds

( g in F \ (x,y) iff g . x <> y )

let g be Element of F; :: thesis: ( g in F \ (x,y) iff g . x <> y )

( g in F \ (x,y) iff ex f being Element of F st

( g = f & f . x <> y ) ) ;

hence ( g in F \ (x,y) iff g . x <> y ) ; :: thesis: verum

for g being Element of F holds

( g in F \ (x,y) iff g . x <> y )

let x, y be set ; :: thesis: for g being Element of F holds

( g in F \ (x,y) iff g . x <> y )

let g be Element of F; :: thesis: ( g in F \ (x,y) iff g . x <> y )

( g in F \ (x,y) iff ex f being Element of F st

( g = f & f . x <> y ) ) ;

hence ( g in F \ (x,y) iff g . x <> y ) ; :: thesis: verum