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